I will look through Ralf's Ramblings and I also found this paper: Stacked Borrows: An Aliasing Model for Rust by Ralf Jung et. al.
I assume this isn't yet "standardized" as in "stable" yet but proposals to describe the way how Rust currently works like or should work like?
I.e. can I really be sure that my very first example is sound? Is this only due to non-documented behavior of the compiler, which I might be able to rely on though due to some sort of "de-facto stability" and Rust's stability gurantees?