Instead, I can concentrate on the interesting questions coming up in the unsafe code guidelines:
What exactly do the guarantees "mutable borrows don't have aliases" and "the pointees of shared borrows are not mutated" *mean*? How should they be reflected in a semantics of MIR -- in miri -- such that the desired [optimizations](https://github.com/nikomatsakis/rust-memory-model/tree/master/optimizations) are actually legal, while at the same time the [unsafe code](https://doc.rust-lang.org/nomicon/) people write has the desired behavior?
Instead, I can concentrate on the interesting questions coming up in the unsafe code guidelines:
What exactly do the guarantees "mutable borrows don't have aliases" and "the pointees of shared borrows are not mutated" *mean*? How should they be reflected in a semantics of MIR -- in miri -- such that the desired [optimizations](https://github.com/nikomatsakis/rust-memory-model/tree/master/optimizations) are actually legal, while at the same time the [unsafe code](https://doc.rust-lang.org/nomicon/) people write has the desired behavior?