Re: Proving Axiom Correct -- at the C level

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct -- at the C level

Tim Daly
I previously mentioned the "proof tower" approach to the question
of proving code at many different layers. Spad code proven in COQ,
Lisp code in ACL2, and Intel code in CCAs. The missing step in the
tower was C.

Apparently there is work in COQ (http://robbertkrebbers.nl/research/ch2o/)
on the CH2O formalization of ISO C11 by Robbert Krebbers. CH2) provides
an operational, executable, and axiomatic semantics for a significant
fragment of C11. So this provides COQ support for the missing layer in
the proof tower.

Now all we need are Category props and Domain proofs. What could be easier? :-)

Tim


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
C Y
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct -- at the C level

C Y
> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly <[hidden email]> wrote:
> I previously mentioned the "proof tower" approach to the question
> of proving code at many different layers. Spad code proven in COQ,
> Lisp code in ACL2, and Intel code in CCAs. The missing step in the
> tower was C.

Rather than introduce another complex language and proof problem into the stack, would it be possible to have Lisp implemented directly "on the metal"?  If SBCL isn't the preferred approach to such a system, maybe the following project could be used as a starting point to put together a purpose built LISP?


Maybe some of the open source "LISP as OS" projects could offer lower level primitives from which to build the boot strapping code, or a basic set could be defined in x86-64...  I suppose it's academic at this point, but I can't help wondering if there would be simplicity gains in the "expressing and defining proof stacks" department that would make it worthwhile in the long run to hold the number of conceptual expression languages down to the minimum necessary.

CY

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct -- at the C level

Tim Daly
Yes, I'd like to have a solid "floor" to the proofs and the fewer layers, the better.

An issue arises when looking to prove the propositions for the Domain
NonNegativeInteger (NNI). This is closely related to the 'nat' domain in proof
systems. However, NNI relies on calls to Lisp for things like defining
equality. Lisp equality is a much-discussed question involving EQ, EQUAL,
etc. which eventually gets resolved down to the machione level. So no
matter which lisp is used, the machine gets involved it seems.

If I "misunderstand" Homotopy Type Theory there is an axiom of
"Univalence" which states that equality is equivalence. Given that,
it might be possible to establish a "floor" at the Spad level so we
do not even have to provide proofs of lisp and below. For me this
is an open research question.

I am still studying the HoTT work. I haven't seen it used for algorithms
like Groeber basis. There is some interesting work by Andre Platzer
which uses substituion as the basis of sound reasoning.
http://dx.doi.org/10.1007/s10817-016-9385-1
From my limited understanding so far it appears to be similar to
Hoare triples on steroids. This might prove very useful for handling
imperative programs. Again, for me this is an open research question.

Here's some things he's been doing in the realm of real arithmetic
http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf
Generally, rigorously proving valid facts of first-order real arithmetic / unsatisfiability
of a set of polynomial inequalities is quite important for his work. He does some
nice things with Groeber basis.

I've collected the "category tower" in Axiom for NNI along with their
associated propositions. I'm trying to do something trivial by hand so
I can understand the research questions better. When I get an example
I'll post the results here.

Tim




On Wed, Apr 5, 2017 at 9:24 PM, C Y <[hidden email]> wrote:
> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly <[hidden email]> wrote:
> I previously mentioned the "proof tower" approach to the question
> of proving code at many different layers. Spad code proven in COQ,
> Lisp code in ACL2, and Intel code in CCAs. The missing step in the
> tower was C.

Rather than introduce another complex language and proof problem into the stack, would it be possible to have Lisp implemented directly "on the metal"?  If SBCL isn't the preferred approach to such a system, maybe the following project could be used as a starting point to put together a purpose built LISP?


Maybe some of the open source "LISP as OS" projects could offer lower level primitives from which to build the boot strapping code, or a basic set could be defined in x86-64...  I suppose it's academic at this point, but I can't help wondering if there would be simplicity gains in the "expressing and defining proof stacks" department that would make it worthwhile in the long run to hold the number of conceptual expression languages down to the minimum necessary.

CY


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