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?

# Math behind borrow checker

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.

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.

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: https://www.youtube.com/watch?v=_agDeiWek8w&list=PLgC1L0fKd7UkVwjVlOySfMnn80Qs5TOLb&index=4

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: http://www.ats-lang.org/MYDATA/VsTsVTs-2018-10-28.pdf

They're on ATS, which uses linear types; Rust uses affine types.