Idris
Dependently typed functional language — types can express arbitrary program properties, enabling proof-carrying code.
static
compiled
since 2007
functionaldependent-types
Idris extends the Curry-Howard correspondence to its logical conclusion — a dependent type system where the distinction between programs and proofs dissolves. You can write a type that says “this function returns a sorted list” and the compiler will enforce it. Idris 2 is built on Quantitative Type Theory and compiles to native code via Chez Scheme.