Against Borrowing: Own the forest, not the trees!
summary
Argues that Rust’s borrow checker is best understood as an ownership types system layered over classic OO ownership, not a novel separate mechanism; demonstrates formal modeling work (Dafny prototypes and citations to Flexible Alias Protection, region/type papers) and explains how move/copy semantics and stack frames become ownership domains allowing safe circular and linked structures; claims borrowing is largely an epiphenomenon constrained by ownership, reports a Dafny implementation that both clarifies and exposes difficulties, and proposes multiple-owner stack frames to make common data structures easier and provably safe.
AI-written summary · about
chapters (9)
- 0:00Borrowing and ownership intro
- 3:52Goblin Wood ownership metaphor
- 8:06Ownership models in Rust
- 13:04Ownership rules and lifetimes
- 20:48Ownership types and heap
- 23:37Copy and move semantics
- 28:17Ownership and stack frames
- 32:56Why borrowing is unnecessary
- 35:26Q&A
related talks
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing
40mAdvanced Rust Programming Techniques
53mThe Rust Borrow Checker - A Deep Dive
28mYou Don't Own Me
50mRust's Borrow Checker Proven Correct!
36mThe Rust Borrow Checker: A Deep Dive
28mDetecting Borrow and Provenance Bugs Across Unsafe Rust [...]
20mTree Borrows