From: Ralf Jung Date: Sun, 20 Oct 2019 12:53:25 +0000 (+0200) Subject: cross-post linking to SIGPLAN Rust post X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/76651223ecf9417eb2bba6f47c12a5ab3934a325 cross-post linking to SIGPLAN Rust post --- diff --git a/personal/_posts/2019-10-20-type-soundness.md b/personal/_posts/2019-10-20-type-soundness.md new file mode 100644 index 0000000..a8b9dbb --- /dev/null +++ b/personal/_posts/2019-10-20-type-soundness.md @@ -0,0 +1,14 @@ +--- +title: 'What Type Soundness Theorem Do You Really Want to Prove?' +categories: rust research +--- + +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". +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. +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*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/)