Theorem Proving and Code Generation

According to the Curry-Howard isomorphism a type in a programming language is essentially the same thing as a proposition and an object or program of the type is a(n intuitionist) proof of the proposition. So an automatic proof generator should also be usable to generate objects or programs of a given type. This is exactly what Djinn does. It seems pretty neat.

(I only learned about the Curry-Howard isomorphism in the last couple of years but it's probably of general interest. So I recommend reading the Wikipedia article I link to if you haven't met it before. It's also probably not what you're currently guessing it is. It's not about program correctness but type correctness and it doesn't prove programs to be correct but shows how programs themselves are proofs of type correctness. In the language of the article, Djinn solves the "Type Inhabitation Problem".)