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-1From 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