Rust has demonstrated that static type systems can grant programmers explicit control or their programs’ memory management, within the context of a practical systems programming language. Rust’s design draws on more than 30 years of work across many different programming language research communities: monadic programming, linear functional programming, region allocation (PLDI), ownership types (OOPSLA), alias burying, fractional permissions (ECOOP).

Taking an historical approach, this tutorial will attempt to weave a coherent narrative out of these seperate yet intertwining threads. We’ll show how Rust (and Pony, Verona, Gallifrey, and Dafny etc) draw on this research. We’ll describe the similarities and difference between these more imperative approaches, and functional approaches ranging from the recent Linear Haskell extensions, MLKit regions, back to clean in the 1980s Clean. We’ll also consider how ownership techniques have been applied in program verification, from Eiffel, Fresco, and Spec#, to JML and Dafny, and how they relate to congate approaches such as separation logics, regional logics, and dynamic frames. Finally we’ll outline possibilities for future research directions and developments.