Comment by lopatin

I started using Idris a few years ago because the idea is fascinating. Such as state machines in your type system, the size of a list being defined in the static type system, even if the list size changes over time (pretty mind blowing), etc..

But ultimately I realized that I’m not writing the type of software which requires such strict verification. If I was writing an internet protocol or something like that, I may reach for it again.