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
_______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
