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 CH2
>Perhaps there are issues around this that will matter? Given that there
>are two formulations of each algebra, one like this:
>zero: () -> $
>succ: ($) -> $
>and one like this:
>+ ($,$) -> $
>If one form is needed for inductive proofs and the other form for
>applied mathematics. Could Axiom ho
On 31/03/17 05:34, Tim Daly wrote:
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does n
