# Machine math, clarification

beeson@cats.UCSC.EDU
From: beeson@cats.UCSC.EDU
Date: Wed, 21 Apr 93 09:07:26 -0700
Message-id: <9304211607.AA08993@si.ucsc.edu>
To: chou@CS.UCLA.EDU, qed@mcs.anl.gov
Subject: Machine math, clarification
Sender: qed-owner
Precedence: bulk

Clarification inspired by Bob Boyer's remark: Machine Math MUST
be a formal language, with a precise syntax and semantics. However,
it must be UNLIKE currently known formal languages in that it must
NOT be repulsive to mathematicians. This must be accomplished by
making the syntax of Machine Math sufficiently similar to what
mathematicians currently write in journals.
I have a good deal of experience (seven years of programming)
building a system that incorporates precise rules for calculus, algebra,
and trigonometry, with the aim of making the computer user-friendly
to students of those subjects, and in particular, of automatically
producing step-by-step solutions as an A+ student should. I learned
that ordinary mathematics DOES have precise rules, even though those
rules require thousands of lines to express rather than dozens.
I believe the same goes for ordinary informal proofs. Machine
Math must solve the following proportion:
Machine Math Lisp or C
______________ _____________
"core logic" machine or assembly code
Some kind of "core logic" (a minimal logical apparatus) is inevitable,
for implementations, just as machine code can't be avoided if you want
to run algorithms.