Also! I did not know that Odersky & associates are working on a clean reimplementation of Scala called "Dotty" that is named after exactly this kind of type theory (Dependent Object Types or DOT).<p>They just got their compiler to self-host, see <a href="https://github.com/lampepfl/dotty" rel="nofollow">https://github.com/lampepfl/dotty</a> and <a href="http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html" rel="nofollow">http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-boo...</a>
The first formal type system that works for (simplified) Scala.<p>More generally, shifting from term rewriting to operational semantics (i.e. proving interpreters correct) seems like a big improvement. Instead of working in a completely different semantic domain, we work in one closely allied to our implementations.