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.