[Axiom-developer] Proving Axiom correct

[daly]

The C standard formalized in Coq (http://robbertkrebbers.nl/thesis.html)

This thesis describes a formal specification of the sequential
fragment of the C programming language based on the official
description of the C language, the C11 standard.

Axiom uses GCL which compiles to C.
Axiom has a graphics package written in C.

The tools are becoming available, Coq for Spad, ACL2 for Lisp, and now
Coq for C. Axiom has been restructured to automate the Coq and ACL2
proof machinery. These proofs are run on request at build time.

Ultimately this will lead to higher quality software as well as a
deeper understanding of questions like simplification and branch cuts.

Proving computational mathematics correct is a long term but vital goal. 

Tim