What Type Soundness Theorem Do You Really Want to Prove?

My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the SIGPLAN blog on the idea of “semantic typing”. This is the methodology behind RustBelt, so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on. In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.

The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets. If you are interested in formal methods for type systems and in particular for Rust, you should check it out! It’s a great read:

“What Type Soundness Theorem Do You Really Want to Prove?” on PL Perspectives

Posted on Ralf's Ramblings on Oct 20, 2019.
Comments? Drop me a mail!