Consider Idris. http://www.idris-lang.org/ http://www.idris-lang.org/ - It is an ML family language, with a compiler written in Haskell. This comes with all th

Consider Idris. http://www.idris-lang.org/ http://www.idris-lang.org/ - It is an ML family language, with a compiler written in Haskell. This comes with all the elegance and clean syntax of a modern typed functional language. - It uses a dependent type system, similar to Agda. This means that the types can carry arbitrary proof information. - The infrastructure is built around this. There is a proof assistant to assist you in building proofs that everything works. - Its not entirely unpragmatic, as it actually has a (small) community, and can compile to C and then (somewhat) efficient code. But who cares about that, right? For a really cool example, see this video, where they implement a Semigroup and Monoid instance for an Option type, including proofs that the appropriate laws hold for the implementation: https://www.youtube.com/watch?v=P82dqVrS8ik https://www.youtube.com/watch?v=P82dqVrS8ik