The Algebra of Loans in Rust
The heart of Rust borrow-checking is this: when a borrow is taken, and until it expires, access to the borrowed place is restricted. For example you may not read from a place while it is mutably borrowed. Over the recent months, lively discussions have been happening around teaching the borrow-checker to understand more things than just “shared borrow”/”mutable borrow”. We’re starting to have a few ideas floating around, so I thought I put them all down in a table so we can see how they interact. I’ll start with the tables and explain the new reference types after. To clarify the vocabulary I’ll be using: A “place” is a memory location, represented by an expression like x, *x, x.field etc1; “Taking a borrow” is the action of evaluating &place, &mut place,…
