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?
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.
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.