Some other projects that are doing cool things in this space are Idris[1] and F-Star[2] (the latter is also a Microsoft Research project). I am particularly imp

Some other projects that are doing cool things in this space are Idris[1] and F-Star[2] (the latter is also a Microsoft Research project). I am particularly impressed by Idris's algebraic effect approach, since it gives you a general effect system that combines the ability to easily extend that monad transformer approaches provide with the ease of use and inference of F*'s effect system. I think the theory behind algebraic effects is a key step in making it easy to develop code with more stringent and customized safety properties than is available in languages like Rust. [1]: http://www.idris-lang.org/ http://www.idris-lang.org/ [2]: https://www.fstar-lang.org/ https://www.fstar-lang.org/