Re: Proving Axiom Correct

Am 13.01.2017 um 07:35 schrieb Tim Daly:

...

> 
> 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

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

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

> _______________________________________________
> Axiom-developer mailing list
> [email protected]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>