Idris is a programming language designed to encourage Type-Driven
In type-driven development, types are tools for constructing programs.
We treat the type as the plan for a program, and use the compiler
and type checker as our assistant, guiding us to a complete program that
satisfies the type. The more expressive the type is that we give up front,
the more confidence we can have that the resulting program will be correct.