Proof-carrying · algorithm-first compiler

RUNE

You describe the algorithm. The compiler chooses the implementation, and proves it correct.

Raidō · the rune of the journey, the choosing of a path.

Kindling the compiler (Python, in your browser)…