Along these lines is an intermediate language called Morte[0], developed by Gabriel Gonzalez, well known in the Haskell community. It seems to still be getting

Along these lines is an intermediate language called Morte[0], developed by Gabriel Gonzalez, well known in the Haskell community. It seems to still be getting some love. The basic idea is to implement a strongly normalizing calculus of constructions which languages can compile down to. That way, equivalent functions provably generate equivalent code. Here's [1] a blog from 2014 that goes into more detail on motivation, examples, and the like. There's a proof-of-concept frontend called Annah[2]. I'm unaware of any backends though. [0]:https://github.com/Gabriel439/Haskell-Morte-Library https://github.com/Gabriel439/Haskell-Morte-Library [1]:http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html http://www.haskellforall.com/2014/09/morte-intermediate-lang... [2]:https://github.com/Gabriel439/Haskell-Annah-Library https://github.com/Gabriel439/Haskell-Annah-Library