The first six years in the development of Polonius
summary
Polonius aims to extend Rust’s borrow checker to handle conditional early returns (Case 3) by modeling lifetimes as sets and letting the outlives graph vary with control flow. Work begins in 2018 with an Datalog prototype on nightly that proves correctness but fails on memory and speed. The current path removes higher‑kinded logic from borrow checking, ports rules into a Rust/Datafrog engine, and experiments with a flip perspective and a tiered borrow check; a performant, stable prototype is still unfinished.
AI-written summary · about
chapters (16)
- 0:00Polonius introduction
- 1:02Rust and ownership types
- 3:49Borrow checker rules
- 7:02Lifetime inference evolution
- 10:35Edge cases limitations
- 12:01Polonius changes
- 14:08Polonius history
- 15:32Polonius and Datalog
- 16:58Datalog challenges
- 18:01Incremental integration plan
- 19:26Borrow Checker improvement
- 20:30Dynamic graphs reasoning
- 21:11Higher-kinded types handling
- 23:21Borrow checking tiers
- 24:01Polonius possibilities
- 25:25Summary
related talks
32mThe First Six Years in the Development of Polonius, an Improved Borrow Checker
53mThe Rust Borrow Checker - A Deep Dive
50mRust's Borrow Checker Proven Correct!
36mThe Rust Borrow Checker: A Deep Dive
22mThe Rust Borrow Checker - A Deep Dive
38mThe Rust Borrow Checker: a Deep Dive
35mPolonius: Either Borrower or Lender Be, but Responsibly
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing