[Axiom-developer] Proving Axiom Correct

[daly]

COQ is being used as the proof engine for Spad-level code.

The latest change will automatically extract literate chunks
labelled 'coq' into a separate location for the COQ proof engine.
This can be controlled from the make command line by adding COQ=coq.

ACL2, with its lisp-based syntax and semantics, is the appropriate
engine for proving the interpreter and compiler. COQ, with its
ability to form dependent types, is the appropriate engine for
proving the algebra. Thus we're able to use the best tool for
each level of abstraction.

Tim