Včera byla vydána verze 0.4.0 jazyka Idris 2. Jedná se o reimplementaci původního experimentálního jazyka Idris, který je podobný Haskellu a obsahuje propracovanou podporu závislostních typů. Podobně jako v případě jazyka Agda je jeho typový systém založený na intuicionistické logice, což je formální logický systém umožňující konstruktivní dokazování matematických tvrzení, čehož se využívá při typové kontrole programů.
