This is a historically moment symbolically. Because Idris is the first new generational general purpose programming language.
What is "new generational"?
Of course it is purely functional, but fortunately after Haskell, Elm, Purescipt : this is not big news these days. So what then? It is built on Calculus of Constructions. That is a computational model that dropped all constraints : types are first class values and types can depend on everything, even on runtime values ["dependent type system"]. This gives it huge expressive power : equivalent with constructive mathematics, which in turn practically can express everything from mathematics in some work-around way. Because this is achieved by dropping constraints, it is very simple too. The amazing beauty in it is the combination of simplicity, intuition, power.
In what sense is it general purpose? Unlike Agda and Haskell [other purely functional languages which have or going to have dependent type-system] : Idris uses strictly eager evaluation order to keep memory usage low. Unlike Agda : Idris is designed to be a programming language first, only after that a mathematical tool.
Why is this release only symbolical? Unfortunately only the language is ready now. Documentation, a compiler, run-time systems also exist, but they are very immature, enough only for brave language enthusiasts or where bug-safety is extremely important. Less than 1 person is working on Idris now, without direct financial support, so fast improving is not yet expected.
the release announcement
