[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Proving Axiom Correct
From: |
Kurt Pagani |
Subject: |
Re: [Axiom-developer] Proving Axiom Correct |
Date: |
Fri, 13 Jan 2017 18:04:53 +0100 |
User-agent: |
Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0 |
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
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>