As far as I can tell, this is another piece of Amal Ahmed's high-level compiler verification project. The idea is that we don't have good tools to compare prog

As far as I can tell, this is another piece of Amal Ahmed's high-level compiler verification project. The idea is that we don't have good tools to compare programs written in different languages, but these tools do exist so long as we stay in the same language. So while it's currently difficult to verify a compiler from a rich functional language to assembly, we have very good tools to verify a compiler from one subset of a language to another. So if we want to verify a compiler from a functional language to assembly we "simply" need a language that is a superset of both, and that's where FunTAL comes in. --- I'm looking forward to reading the paper and it's great that this project is producing some independently useful artifacts. On the other hand I still think that this approach to compiler verification is a bit odd. Time will tell, I suppose...