[Axiom-developer] Correctness/Provability/Compiling

[root]

Functional Pearl, A Type-correct, stack-safe, provably correct
expression compiler in Epigram.
http://www.cs.nott.ac.uk/~jjw/papers/Compiler_Pearl/Compiler_Pearl.pdf


I've mentioned before that it is a long term goal of Axiom to 
enhance the compiler to prove properties of Categores and Domains.
This is of interest because of that goal. I'd like to be able to
do things like decorate the Categories and Domains with mathematical
axioms (e.g. Group) and prove properties like commutative rather
than just assert them. 

Tim