Tutorial on implementing a borrow checker on a simplified language?


In Haskell, there’s the excellent paper Typing Haskell in Haskell which acts as a tutorial on how the Hindley Milner type checker that powers the Haskell compilers work. In the past I’ve used this to write a Hindley Milner type checker on a lambda calculus, as an exercise to understand the internal algorithms of Haskell type checking.

I’d like to do the equivalent thing for Rust: implement a borrow checker for a simple language (say, a variant of a simply typed lambda calculus). Are there any resources that describe the borrow checker’s typing rules in an accessible way, to help me get started on this? Ideal would be a tutorial like the Typing Haskell in Haskell paper linked above, but something like a paper or blog post describing the typing rules would also be useful.


I think the description in the NLL RFC is probably the best one available that’s both detailed enough to actually write an implementation, yet still comprehensible for a sufficiently motivated person that’s not already an expert on borrow checkers.

I’m not personally aware of any similar writeup for today’s “AST borrow check” algorithm.


Excellent, thank you!


There’s also this series of posts by Ticki:


At some point hey had “here’s a borrow checker in 400 lines of code” but I can’t find it…