Is purity dead? Do you consider Idris a theorem prover? It's dependently typed but seems to be designed for writing operational programs rather than proofs.
I'm not familiar enough with Idris to know exactly how state is handled, but yes, Idris is a prover, since it has dependent types.
If you want to verify your programs (and in 99.9% of programs
you probably don't as you get it sufficiently correct by more lightweight techniques such as testing and code-reviews), then purity is fine, since you have to track effects explicitly anyway to prove non-trivial results, and doing this in a pure functional way or say with auxiliary variables in a Hoare-logic are kind-of/sort-of notational variants.
If "prover" just means "has dependent types" then that's a much larger class than it sounds like. I write a lot of Scala, which has dependent types, but most of the code I write is just ordinary web services.
I don't understand the distinction you're drawing. Idris' type level functions are easier to write than Scala's but they don't seem to be able to do anything that Scala ones can't.
