Skip to content
◈ALB Atlas

Idris Alive

Idris
KindProgramming language
Appeared2007
StatusAlive
CreatorEdwin Brady
FamilyML
Sourcewww.idris-lang.org ↗

Dependent types for working programmers — types that mention values, proofs as programs; the same Brady who co-invented Whitespace.

Created by Edwin Brady

Edwin Brady's Idris (2007/2016) — a dependently-typed language for general programming — made proofs programs: types can depend on values, totality is checked, and the compiler verifies.\n\nIdris 2 (2020) is written in itself; it is the practical dependent-typed language Haskell researchers write in.

Sources

  1. idris-lang.org/
  2. en.wikipedia.org/wiki/Idris_(programming_language)