Will Crichton – Helping Developers Use Type Systems for Memory Safety

Abstract
Programming languages are only as effective as the people who can use them. This talk is about my research on helping tens of thousands of developers work with a complex PL, namely Rust. At the heart of Rust is ownership types, a method for ensuring memory safety without garbage collection. My research takes ownership types in two directions. First, to make ownership types more useful to developers, I designed a new devtool for simplifying comprehension of Rust programs via program slicing. The key technique in the slicer is using ownership types to approximate the behavior of unobservable code, which I show is formally sound and empirically precise. Second, to help developers better understand ownership types, I designed a new conceptual model of ownership as permissions which can be automatically visualized for any Rust program. A large-scale deployment of this model in a popular Rust textbook showed that it quantitatively improves learning outcomes.

Bio
Will Crichton is a postdoctoral researcher at Brown University advised by Shriram Krishnamurthi. Will designs systems to amplify the intelligence of programmers, leveraging programming language theory and cognitive psychology to build generalizable and useful tools. His systems have been used by tens of thousands of people to learn and work with the Rust programming language. Will received his PhD from Stanford University in 2022 advised by Pat Hanrahan and Maneesh Agrawala.

Details

• Date: Tuesday, March 12
• Time: 2:00 pm - 3:00 pm
• Category: Special Seminar
• Location: Grier A 34-401A

Host

• Daniel Jackson
• Email: chadcoll@mit.edu