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 > Axiom-developer@nongnu.org > https://lists.nongnu.org/mailman/listinfo/axiom-developer > _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
