Re: [Axiom-developer] Correctness/Provability/Compiling

[Gabriel Dos Reis]

root <address@hidden> writes:

| 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.

We need a clear formulation of the type system for that.  
Adn we also need a clear grammar.

| 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. 

Funny, you should mention that.  In our design for "C++ concepts", we
have provision for that -- though it is not enforced in the typpe
system directtly, but can be used for auxiliary tools.

-- Gaby