Lambda the Ultimate

In the recent years, Idris had a surprisingly uptake in adoption. It used to be, in some ways, the poor sibling of Agda, which can be explained by the fact that it is more programming-oriented than proof-assistance-oriented, and that the userbase for dependently typed programming language was mostly restricted to people interested in proof assistants.

I would guess that this community focus remains true in general, but Idris managed to make enough improvements to its usability to become approachable by less-experts. In particular, while Idris used to be mostly a one-developer (Edwin Brady) show, there are now strictly more than one people actively contributing to the codebase (see github statistics); David Christiansen's PhD work on the language helped not only in terms of code contributions, but also in continuing to increase the language visibility.

I think that this is very good news for the "rich type systems" community. The enthusiasm for Idris among, for example, Haskell programmers, is a sure sign that there is a sizeable community of people that are interested in adopting yet more advanced, yet less-understood type systems and programming language designs. I used to be surprised that languages such as Haskell and OCaml could manage to form a critical mass despite their otherness; Idris is one of today's underdogs (not alone: other dependent languages and proof assistants, such as Coq, Agda, Isabelle, Lean, also made a ton of progress in the last decade), and the interest for them says something positive about the world of programming (and proving): people are curious and interested in advanced topics, even at a cost.

(In particular, as a programming language researcher I would see this as a motivation to keep explaining our work in a way that is accessible to interested programmers -- and non-programmers. They actually care.)