The Usability of Advanced Type Systems: Rust as a Case Study.
Advanced type systems that enforce various correctness and safety
guarantees–such as linear and ownership types–have a long history in the
Programming Languages research community. Despite this history, a
human-centered evaluation of these type systems and their usability was all but
absent, with empirical evaluations limited to testing their expressiveness in
programs written by experts, i.e. the creators of the type system.
In the past few years, this has begun to change with the adoption of a
version of affine types and ownership in the popular Rust programming language.
With the increase in Rust’s popularity, various studies have begun empirically
evaluating the usability of Rust’s Ownership and Lifetime rules, providing a
breadth of qualitative and quantitative information on the usability of such
type systems. They found that despite Rust’s general success in achieving its
promise of safety and performance, these rules come with a steep learning curve
and have been repeatedly cited as a barrier to adopting Rust.
In this report, I provide a brief history of linear types and region-based
memory management, which directly inspired Rust’s type system. I then introduce
Rust’s Ownership and Lifetime rules, and present the state-of-the-art in
academic research into their usability. I discuss both theoretical arguments
and empirical evidence for why these rules are difficult to learn and apply,
and survey existing work on addressing some of these difficulties. I also draw
from broader works in the HCI and CS Education communities to recommend future
work in this area.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.