What is the math or theory behind rust's borrow checker? I think it may give me the required intuition on it. And are there any blog posts (or papers) that discuss this?
If you want a blog post that essentially describes the majority of the borrow checker, then check out the post behind a new borrow checker being worked on: polonius.
There are much easier ways to understand the borrow checker than reading a more technical specification.
3 Likes
Thanks.
The NLL RFC is also a great resource for where borrow checking is already at today. Polonius is the next step, still being developed, and thus not yet as well-documented as the lexical -> non-lexical change.
1 Like
There is a great presentation by Niko Matsakis about about the borrow checker and the new Polonius borrow checker here:
Polonius: Either Borrower or Lender Be, but Responsibly: Polonius: Either Borrower or Lender Be, but Responsibly - Niko Matsakis - YouTube
3 Likes
Stacked Borrows: An Aliasing Model for Rust specifies operational semantics for borrowing, including some formal proofs. This is the model that Miri uses. There is also a series of blog posts introducing the concepts.
4 Likes
Not Rust-specific but Hongwei Xi has a bunch of wonderful papers: http://www.ats-lang.org/MYDATA/VsTsVTs-2018-10-28.pdf
They're on ATS, which uses linear types; Rust uses affine types.
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.