Dependent types-based language Idris will soon reach version 0.99, which can be viewed as an alpha release of 1.0, according to the Idris team. Idris 1.0 is expected sometime around February 2017.
Idris is a purely functional programming language that aims to make type-based program verification techniques available to a larger number of programmers while retaining its focus on being general-purpose and efficient enough to be used for system programming as well.
The main idea behind Idris is that of dependent types, which aim to express dependencies between types and values, just like functions are a way to express dependencies between values. For example, we could define a sort function as returning a list where each element is smaller than the next, so that any implementation of that function will only compile if that property is proved true. Other examples of properties of software that could be expressed through Idris are array bounds verification and protocol correctness in distributed or concurrent systems, such as ensuring that all programs follow a specific protocol when accessing a file handle. This is how you can define a Vect type in Idris and a app function to append two such vectors:
infixr 5 ::;
data Vect : Set -> Nat -> Set where
VNil : Vect a O
| (::) : a -> Vect a k -> Vect a (S k);
vapp : (Vect A n) -> (Vect A m) -> (Vect A (plus n m));
vapp VNil ys = ys;
vapp (x :: xs) ys = x :: vapp xs ys;
In the above code, the compiler is able to detect any misuse of the involved types, such as in the following broken implementation of vapp:
vapp : Vect a n -> Vect a m -> Vect a (plus n m);
vapp VNil ys = ys;
vapp (x :: xs) ys = x :: vapp xs xs; -- BROKEN
The main factor behind the decision to release 1.0 is the language getting stabler, say Idris core developers. This will not mean, though, that the language can be considered be “production ready”, mostly due to the impossibility for the development team to support it in the long term or guarantee the quality of its implementation. Still, Idris retains a lot of its value as a research tool to explore programming using dependent types.
Similarly to Coq, Idris supports interactive theorem-proving, including back reasoning, but aims to be a general-purpose programming language before a theorem prover. Idris compiles to C and relies and uses garbage collection for memory management.
