Re: [Axiom-developer] Proving Axiom Correct

[Tim Daly]

>From: Kurt Pagani <address@hidden>
>
>>
>> Axiom is using Coq for its proof platform because Axiom needs
>> dependent types (e.g. specifying matrix sizes by parameters).
>>
>> In addition, Coq is capable of generating a program from a
>> proof and the plan is to reshape the Spad solution to more
>> closely mirror the proof-generated code. Also, of course, we need
>> to remove any errors in the Spad code found during proofs.
>
>A SPAD extractor should be feasible but it may take some time to set up the
>necessary infrastructure to compile a plugin. E.g. see
>
>https://github.com/coq/coq/tree/trunk/plugins/extraction

I had not actually thought of trying to extract Spad directly.

My plan was to extract the ML code and compare it to Spad.

It would be interesting to extract Spad directly.
Indeed it would probably uncover bugs in Axiom's compiler.

I think it would be really valuable to try to converge Spad and COQ.

It would force more functional programming discipline on Spad code.

COQ will probably benefit as Axiom's mathematics gets proven.

>There is a recent post @ https://news.ycombinator.com/item?id=12183095
>about Coq2Rust where I saw some nice ideas:
>
>-- https://github.com/pirapira/coq2rust
>
>There's more about it if you use the search field (bottom) at
>https://news.ycombinator.com/news.
>
>>
>> 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.
>
>http://pvs.csl.sri.com
>https://github.com/nasa/pvslib/blob/master/interval_arith/interval.pvs

Thanks. I'll look into the PVS work. However, I've looked at a fair number of

these proof systems and COQ seems to be well supported (an INRIA project),

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.