Rust's Borrow Checker Proven Correct!
summary
Claim: borrow checker proven correct for a formal subset of Rust — lifetimes, ownership and aliasing get modeled and the properties are machine-checked. Verification uses Iris (a higher‑order concurrent separation logic) implemented in Iris in Coq, plus comparisons to tools like QuickCheck and Concert/CompCert style methods. The process finds concrete compiler and library bugs, those bugs get fixed, and the result ships as sounder Rust borrow‑checking for real programs.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:13Rusts Borrow Checker
- 6:45Compiler Problems
- 7:53C Problems
- 14:28Type Error
- 15:43Security Vulnerabilities
- 18:34Multiple Aliases
- 20:16Locking
- 22:05Formal Verification
- 25:55Unsafe
- 28:09Nfactorial Explosion
- 29:59Not Testing Code
- 33:38What Could Go Wrong
- 34:15Send Receive
- 35:46Coding Use
- 38:10The Pointer
- 39:48Double Withdrawal
- 41:18Wrapping
related talks
53mThe Rust Borrow Checker - A Deep Dive
36mThe Rust Borrow Checker: A Deep Dive
22mThe Rust Borrow Checker - A Deep Dive
38mThe Rust Borrow Checker: a Deep Dive
05mEmulating Rust's Borrow Checker in C++
26mThe first six years in the development of Polonius
28mDetecting Borrow and Provenance Bugs Across Unsafe Rust [...]
32mThe First Six Years in the Development of Polonius, an Improved Borrow Checker