The Algebra of Loans in Rust
19 points by runxiyu
19 points by runxiyu
This is not an algebra. It is a sketch of some ideas, pre formalization.
I think any significant revs of the memory model deserve a formalization and a proof of correctness, to be quite honest. We have enough production code in Rust that the bar to changes should be quite high. (I think we have 300kLoC of Rust doing valuable computations at my fine shop, we're just one of many).
So far there is no official memory model, see https://doc.rust-lang.org/reference/memory-model.html, although there is https://rust-lang.github.io/fls/ and what miri assumes https://github.com/rust-lang/miri with respective publications on formal models. I do assume that Ferrous Systems is improving that (towards getting a formal one) to get approval for higher safety and security status of their compiler.