Kurt,
I've been using Proof General for COQ proof development.
I've been thinking about your idea of directly proving Spad code.
There are several interesting points.
COQ has types as first-class objects. This allows types like
nat to be effectively renamed into NNI. More likely, a COQ-based
NNI would extend COQ's nat type. It appears I can also do some
Spad-Category-like inheritance hierarchy. The net result would be
that "nearly native" Spad code could be proven.
COQ also has a form of literate programming. COQ comments are
rendered as latex/pdf files. Latex commands can be embedded in the
comments. The net result is that a form of the final document is
directly executable.
Proof General runs the coqtop interpreter as a separate process under
Emacs, similar to the Slime interface used for lisp. This allows for the
forward and backward stepping in the file. Axiom has an undo command
so it seems possible to run the Axiom interpreter under Proof General.
That would allow interactive development of Spad code that could also
be proof-checked during development.
This combination of factors could really change the way that Axiom code
is developed, leading to much higher code quality.
If I get time this semester I may try to develop the geometric algebra code
this way. It depends on how the class goes.
All things considers, you made a brilliant suggestion.
Tim