[Users] Automated code generation with correctness proofs

Erik Schnetter schnetter at gmail.com
Fri Nov 6 15:13:40 CST 2020

Since we're discussing automated code generation at the moment, and
since I just learned about Spiral, let me point you to

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 Schnetter <schnetter at gmail.com>

More information about the Users mailing list