From 76651223ecf9417eb2bba6f47c12a5ab3934a325 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 20 Oct 2019 14:53:25 +0200 Subject: [PATCH 1/1] cross-post linking to SIGPLAN Rust post --- personal/_posts/2019-10-20-type-soundness.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 personal/_posts/2019-10-20-type-soundness.md 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/) -- 2.30.2