Math behind borrow checker

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.



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:


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.


Not Rust-specific but Hongwei Xi has a bunch of wonderful papers:

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.