> Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)

AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...