[Users] Automated code generation with correctness proofs

[Erik Schnetter]

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

-- 
Erik Schnetter <schnetter at gmail.com>
http://www.perimeterinstitute.ca/personal/eschnetter/