>There is a recent post @ https://news.ycombinator.com/item?id=12183095
>about Coq2Rust where I saw some nice ideas:
>There's more about it if you use the search field (bottom) at
>> It seems there must be an isomorphism between Coq and Spad.
>> At the moment it seems that Coq's 'nat' matches Axiom's
>> NonNegativeInteger. Coq also has a 'Group' type which needs
>> to be matched with the Axiom type. The idea is to find many
>> isomorphisms of primitive types which will generate lemmas
>> that can be used to prove more complex code.
>Still there are a lot of Lisp dependencies, e.g. integer.spad
>zero? x == ZEROP(x)$Lisp
>-- one? x == ONEP(x)$Lisp
> one? x == x = 1
> 0 == 0$Lisp
> 1 == 1$Lisp
> base() == 2$Lisp
This proof effort uses COQ for the Spad code and ACL2 for the Lisp code.
We will probably need a COQ.Lisp interface package that provides proofs
of Axiom's $Lisp package calls. This needs to be formalized anyway. There
should be a complete list made.
At the moment (in book volume 5) there is a chapter that contains the Lisp
code that Axiom uses but it does not cover direct lisp package calls like 0$Lisp.
I''ll try to collect all instances and document the complete set.
>which will it make necessary to start defining a bunch of axioms/parameters.
>Coq certainly is the right tool for such a venture, however, I recently cloned
'>pvslib' which uses SRI's PVS and I was surprised how close it is
>(syntactically) to SPAD. i guess it would be my second choice.
Thanks. I'll look into the PVS work. However, I've looked at a fair number of
well documented, and compatible with Axiom's needs.
ACL2 is also well supported, well documented, and compatible. I've used some
prior work years ago on a project at IBM Research. It was known as the
Boyer-Moore theorem prover.