Comment by kibwen

Recent blog post from Ralf Jung providing some extra context: https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html

Bonus: recent talk from Ralf Jung on his group's efforts to precisely specify Rust's operational semantics in executable form in a dialect of Rust: https://youtube.com/watch?v=yoeuW_dSe0o