Programmers learning Rust struggle to understand ownership types, Rust's core mechanism for ensuring memory safety without garbage collection. This paper describes our attempt to systematically design a pedagogy for ownership types.
- We studied Rust developers' misconceptions of ownership to create the Ownership Inventory, a new instrument for measuring a person's knowledge of ownership. We found that Rust learners could not connect Rust's static and dynamic semantics, such as determining why an ill-typed program would (or would not) exhibit undefined behavior.
- We created a conceptual model of Rust's semantics that explains borrow checking in terms of flow-sensitive permissions on paths into memory.
- We implemented a Rust compiler plugin that visualizes programs under the model.
- We integrated the permissions model and visualizations into a broader pedagogy of ownership by writing a new ownership chapter for The Rust Programming Language, a popular Rust textbook.
- We evaluated an initial deployment of our pedagogy against the original version, using reader responses to the Ownership Inventory as a point of comparison. Thus far, the new pedagogy has improved learner scores on the Ownership Inventory by an average of 9% (N = 342, d = 0.56).
Thu 26 OctDisplayed time zone: Lisbon change
Thu 26 Oct
Displayed time zone: Lisbon change
11:00 - 12:30 | |||
11:00 18mTalk | Reference Capabilities for Flexible Memory Management OOPSLA Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Microsoft Azure Research, Sophia Drossopoulou Imperial College London, James Noble Research & Programming, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University DOI Pre-print | ||
11:18 18mTalk | A Grounded Conceptual Model for Ownership Types in Rust OOPSLA DOI Pre-print | ||
11:36 18mTalk | Inference of Resource Management Specifications OOPSLA Narges Shadab University of California at Riverside, PRITAM MANOHAR GHARAT Microsoft Research, Shrey Tiwari Microsoft Research, Michael D. Ernst University of Washington, Martin Kellogg New Jersey Institute of Technology, Shuvendu K. Lahiri Microsoft Research, Akash Lal Microsoft Research, Manu Sridharan University of California at Riverside DOI | ||
11:54 18mTalk | Resource-Aware Soundness for Big-Step Semantics OOPSLA Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa DOI | ||
12:12 18mTalk | Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA Andrea Lattuada VMware Research, Travis Hance Carnegie Mellon University, Chanhee Cho Carnegie Mellon University, Matthias Brun ETH Zurich, Isitha Subasinghe UNSW Sydney, Yi Zhou Carnegie Mellon University, Jon Howell VMware Research, Bryan Parno Carnegie Mellon University, Chris Hawblitzel Microsoft Research DOI |