# Proving Axiom Correct

7 messages
Open this post in threaded view
|

## Proving Axiom Correct

 I'm making progress on proving Axiom correct both at the Spad level and the Lisp level. One interesting talk by Phillip Wadler on "Propositions asTypes", a very entertaining talk, is here:https://www.youtube.com/watch?v=IOiZatlZtGUHe makes the interesting point late in the talk that some languages are "discovered" based on fundamental logic principles (e.g.Lisp) and othersare "invented" with no formal basis (e.g. C). As he says, "you can tellwhether your language is discovered or invented".The point is that Lisp has a formal logic basis and, as Spad is reallyjust a domain specific language implemented in Lisp then Spad sharesthe formal logic basis. _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Open this post in threaded view
|

## Re: Proving Axiom Correct

 There were implementations of C in Lisp. So C shares that formal logic basis, or that it was discovered?On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly wrote:I'm making progress on proving Axiom correct both at the Spad level and the Lisp level. One interesting talk by Phillip Wadler on "Propositions asTypes", a very entertaining talk, is here:https://www.youtube.com/watch?v=IOiZatlZtGUHe makes the interesting point late in the talk that some languages are "discovered" based on fundamental logic principles (e.g.Lisp) and othersare "invented" with no formal basis (e.g. C). As he says, "you can tellwhether your language is discovered or invented".The point is that Lisp has a formal logic basis and, as Spad is reallyjust a domain specific language implemented in Lisp then Spad sharesthe formal logic basis. _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Open this post in threaded view
|

## Re: Proving Axiom Correct

Open this post in threaded view
|

## 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/extractionThere is a recent post @ https://news.ycombinator.com/item?id=12183095about Coq2Rust where I saw some nice ideas: -- https://github.com/pirapira/coq2rustThere'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.comhttps://github.com/nasa/pvslib/blob/master/interval_arith/interval.pvs> _______________________________________________ > Axiom-developer mailing list > [hidden email] > https://lists.nongnu.org/mailman/listinfo/axiom-developer> _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer
Open this post in threaded view
|