[Axiom-developer] COQ and Axiom

[daly]

Axiom has a project goal of Proving Axiom Correct. This is
computational mathematics. It needs a solid foundation.

There are limits to what can be proven, of course, but the power
of the proof systems has really improved since Axiom was born.

Of the half-dozen or more proof systems and it appears that COQ 
is closest to Spad in spirit. COQ has the ability to handle dependent
types (e.g. specifying that an array has a fixed known length). COQ
has the ability to generate OCAML programs from proofs. This will
make it easy to compare with the Spad implementations. A major win
in the long term would be to auto-generate the Spad code but that's
a distant dream at the moment.

Axiom is being attacked from two directions. The first is from the
"categories down", trying to specify Axiom's category signatures in
COQ. The second is from the "bits up", trying to specify the lisp
functions that are implemented using only common lisp primitives.
These are marked in the interpreter already and will soon have
OCAML-like type signatures.

If anyone knows of prior work on either path, please let me know.

We have already gotten permission from Laurant Thery to use his work
on the proof of Buchberger's algorithm, some of which will show up
in Volume 13. I have to reverse-engineer his proof into the Spad
implementation.

Tim