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