[catnaroek]

Sadly, AFAIK, Idris does not have linear types out of the box. I am aware that you can prove you are properly releasing your resources using dependent types, so technically speaking there is no loss of expressivity. However, having the compiler do the checking and enforcement automatically is a huge usability win in my book, especially since juggling with the lifetimes of various resources is such a common task in systems programming.

That aside, Idris looks very promising for verified application development.