I suggest you email the team that did the C formal semantics about doing one for Rust. They did it in K Framework (Maude-based) with a front end, KCC, designed

I suggest you email the team that did the C formal semantics about doing one for Rust. They did it in K Framework (Maude-based) with a front end, KCC, designed to be usable like GCC. Their other work includes functional and logic languages. A team that did an executable semantics for all of those seems ideal for a formalized compiler for Rust given it's like several styles combined. Their rewriting based tools could probably handle at least a subset. Then you get DDC for free plus a way to equivalence check reference compiler for certain features. https://github.com/kframework/c-semantics https://github.com/kframework/c-semantics http://www.kframework.org/index.php/Main_Page http://www.kframework.org/index.php/Main_Page