Idris

Website: idris-lang.org

Designed by: Edwin Brady

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker.

Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.

The Idris type system is similar to Agda’s, and proofs are similar to Coq’s, including tactics (theorem proving functions/procedures) via elaborator reflection.

Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages.

Idris compiles to C (relying on a custom copying garbage collector using Cheney’s algorithm) and JavaScript (both browser- and Node.js-based).

There are third-party code generators for other platforms, including Java virtual machine (JVM), Common Intermediate Language (CIL), and LLVM.Idris is named after a singing dragon from the 1970s UK children’s television program Ivor the Engine.