Idris

Created by Edwin Brady, first released in 2007 (Idris 2 in 2020). A general-purpose language with dependent types — like Haskell but types can depend on values. Bridges the gap between theorem provers and practical programming.