[Top][All Lists]

[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

There is a recent post @
about Coq2Rust where I saw some nice ideas:


There's more about it if you use the search field (bottom) at

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

> _______________________________________________
> Axiom-developer mailing list
> address@hidden

reply via email to

[Prev in Thread] Current Thread [Next in Thread]