On: I tried Haskell for 5 years

[devrandomguy]

Yes, the author mentioned Idris shortly afterwards, but I get the impression that this is just the tip of an iceberg. Idris was presented as the one example that is most likely to evolve from a research-only language, to a production language.

[dllthomas → devrandomguy]

There's also agda and coq, at various points on the spectrum between programming language and theorem prover.