[Users] Automated code generation with correctness proofs

Since we're discussing automated code generation at the moment, and since I just learned about Spiral, let me point you to http://spiral.net/index.html.

Spiral is an automated code generator for compute kernel that starts from a mathematical description in Coq, an automated theorem prover, and works from there all the way down to efficient assembler code. (I'm not suggesting to use it for the Einstein Toolkit, since it's very important for us that the generated code ties nicely into Cactus.) However, being able to automatically go e.g. from the definition of a Fourier Transform to highly efficient machine code is quite exciting.

-erik