axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] Proving Axiom Correct -- at the C level

 From: Tim Daly Subject: Re: [Axiom-developer] Proving Axiom Correct -- at the C level Date: Thu, 6 Apr 2017 07:08:44 -0400

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 wrote:
> On Friday, March 31, 2017, 7:16:32 PM EDT, Tim Daly <address@hidden> 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