Re: [Axiom-developer] Computational Mathematics, proofs, and correctness

[jiazhaoconga]

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/