I previously mentioned the "proof tower" approach to the question of proving code at many different layers. Spad code proven in COQ,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 |
> 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 |
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 is an open research question. 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/s108 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:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |