Towards a linear functional translation for borrowing
summary
Claims a mechanical translation from Rust mutable borrows to a pure linear functional program that preserves Rust’s linearity guarantees and relies on existing Aeneas/NS ideas; uses explicit region annotations from the borrow checker (no lifetime inference), represents regions as roots as linear functions, translates borrows to their underlying values and implements drops by calling those roots, and maps region bounds to region→function dependency so call order enforces aliasing rules. Works as a paper proof for a small fragment; implementation remains work in progress.
AI-written summary · about
chapters (6)
- 0:00Linear functional translation intro
- 1:04Motivation and Rust mut borrows
- 3:35Borrow checker invariants examples
- 8:36Regions and lifetime bounds
- 13:17Functional translation of borrow proofs
- 21:25Conclusion and future work
related talks
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing
15mAeneas: Rust Verification by Functional Translation
26mThe first six years in the development of Polonius
36mThe Rust Borrow Checker: A Deep Dive
40mAgainst Borrowing: Own the forest, not the trees!
22mThe Rust Borrow Checker - A Deep Dive
53mThe Rust Borrow Checker - A Deep Dive
32mThe First Six Years in the Development of Polonius, an Improved Borrow Checker