I want to like Idris - as a language it does so much right - but I still feel a little burnt. A few years ago were exciting times; Idris 1 had hit 1.0 and was h

I want to like Idris - as a language it does so much right - but I still feel a little burnt. A few years ago were exciting times; Idris 1 had hit 1.0 and was humming along nicely, there was excellent tooling available, & Type-Driven Development with Idris had been published - a real printed book about practical coding with dependent types! Could reliable software be far behind? Would I maybe get to develop somewhere that took software engineering seriously in my lifetime? And then, with the possibility of success on the horizon, the Idris folk(s) got distracted by the QTT hype and decided to abandon ship so they could start on Idris 2. And, like, don't get me wrong - the QTT stuff is cool, and I'm a Rust fan in part because getting to encode linearity in your types is a real superpower - but it's so depressing that the world of practical dependent types feels just as far away now as it did ten years ago, after getting so excited about it five years ago. And it underscores what might be a bigger problem: at the end of the day - and by the Idris FAQ's own admission - Idris is a research project into practical dependent types, and Edwin Brady is an academic. Which means that when he gets interested in some other area of research, he's free to just...do that instead, or start over on Idris n+1, and leave Idris 1, 2, 3 ... n to wither.