[Axiom-developer] Proving Axiom correct

[daly]

Leslie Lamport has an interesting talk on hierarchical proofs.

If you have any interest in proving Spad programs correct then this
is an interesting talk[1]

I've been looking at various tools to prove Spad algorithms at all
layers (math->spad, spad->lisp, lisp->C, C->machine) In particular,
I'm focusing on the GCD algorithm in EUCDOM as the proof of the
algorithm is widely known. The first step of this kind of proof is to
do the (math->spad) phase.

Lamport has a system called TLA which allows hierarchical structuring
of proofs in math. COQ does machine-checked proofs, especially those
with types. Since Axiom is hierarchical it seems that TLA can
structure the proof into sub-proofs (e.g.  showing that unitCanonical
is correct) and COQ can be used to focus on each layer.

In any case, it is time to try to take baby-steps toward putting Axiom
on a firm mathematical foundation.

If you know of any other interesting lectures please let me know.

Tim

[1] http://hits.mediasite.com/mediasite/Play/29d825439b3c49f088d35555426fbdf81d