I have some experience with ACL2, ACL2 uses a very small subset of common lisp, there are no side effects and no higher order functions, although Axiom is written in a pretty small subset of CL, it will be very difficult or require unimaginable mount of work to prove "the Spad compiler is correct" (this Axiom implementation of Spad language compiler agrees with Spad language specification).
As for the second interpretation, I am not familiar with Coq. I can only mention about PVS [1], a common lisp theorem prover but unlike ACL2 which is first-order and weak typing, PVS and Coq are high-order and strong typing. But I am not familiar with PVS either. [1] PVS http://pvs.csl.sri.com/ _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
