Idris

Idris is a dependently typed programming language designed by Edwin Brady, distinguished from other languages in its class by an explicit commitment to being a practical tool for general-purpose programming rather than a research system for constructive mathematics. While Agda and Coq treat programs as proofs and prioritize logical consistency, Idris prioritizes program execution, adding features like strict evaluation, a foreign function interface, and compilation to native code through a C backend. The language is built on a variant of dependent type theory but relaxes some of the totality constraints that make Agda a consistent logic, accepting partial functions in exchange for programming convenience.

The central design tension in Idris is between the precision of dependent types and the pragmatism of industrial software development. A dependent type system can prove that an array index is in bounds, but the proof may require more code than the operation it protects. Idris addresses this through type-driven development, an interactive methodology in which the compiler guides the programmer through proof obligations using holes and refinement, similar to Agda's interaction model but with more aggressive automation. The language also provides a tactic system for proof search, though it is less mature than those of Coq or Isabelle.

Idris has been used to verify network protocols, resource management, and cryptographic implementations — domains where the gap between specification and implementation is expensive and where the precision of dependent types justifies the overhead of formalization. The language has not achieved the community scale of Lean or the industrial deployment of Coq, but it remains a crucial data point in the debate about whether dependent types can escape the proof assistant niche and become a mainstream programming paradigm. The evidence so far is mixed: the languages are powerful, but the programmers are scarce, and the tooling remains immature compared to conventional ecosystems.