Yes! I've also seen the similarities between all of these things and LLVM. Part of LLVM is an interest in correctness. I've seen more of an interest in these a

Yes! I've also seen the similarities between all of these things and LLVM. Part of LLVM is an interest in correctness. I've seen more of an interest in these areas in research as well. For example, there was even a recent research highlight in an ACM magazine about "Formal Verification of a Realistic Compiler": http://pauillac.inria.fr/~xleroy/publi/compcert-CACM.pdf http://pauillac.inria.fr/~xleroy/publi/compcert-CACM.pdf Plus, newer companies like Coverity (http://www.coverity.com/html/research-library.html http://www.coverity.com/html/research-library.html) bring a sense of credibility to a practice that hasn't had much traction in the industry. I think all of these ideas can come together to make something quite useful. But I suppose bringing it all together is the hard part :) Update: I also saw lots of cool associations to the Self Programming Language (http://research.sun.com/self/language.html http://research.sun.com/self/language.html), which includes some great research, especially in their paper "Self: The Power of Simplicity": http://research.sun.com/self/papers/self-power.html http://research.sun.com/self/papers/self-power.html