2 title: 'What Type Soundness Theorem Do You Really Want to Prove?'
3 categories: rust research
6 My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the [SIGPLAN blog](https://blog.sigplan.org/) on the idea of "semantic typing".
7 This is the methodology behind [RustBelt](https://plv.mpi-sws.org/rustbelt/popl18/), 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.
8 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.
10 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.
11 If you are interested in formal methods for type systems and in particular for Rust, you should check it out!
14 > ["What Type Soundness Theorem Do You Really Want to Prove?" on *PL Perspectives*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/)