>Perhaps there are issues around this that will matter? Given that there
>are two formulations of each algebra, one like this:
>zero: () -> $
>succ: ($) -> $
>and one like this:
>+ ($,$) -> $
>If one form is needed for inductive proofs and the other form for
>applied mathematics. Could Axiom hold both forms in a single
>category/domain and switch between them as needed?
Indeed this is a fundamental question.
Holding both forms is not the correct path
since it keeps the "mathematical form" separate from the
"computational form". The point of this work is to "ground"
computational mathematics. So it is necessary to
unify these two forms.
The approach to this problem relies on the fact that Axiom has
proofs not only at the spad layer (using COQ) but also at the
lisp layer (using ACL2). After that comes C and then Intel. There
is a "proof tower" architecture (I failed to mention):
Spad: COQ
Lisp; ACL2
C: ? (Frank Pfenning at CMU has OC, a proven subset
and there is some LLVM based work I've seen)
Intel: I spent 6 years developing the semantics of the Intel
Instruction Set as a Lisp program. It goes from binary
to Conditional Concurrent Assignments which can be
used for reasoning about hardware state:
When you drill down to the spad implementation of equality you find
calls to lisp functions. One of the open research questions is how