In addition, it is entirely possible that when Rust has a formal semantics, it will use exactly such a provenance-aware memory object model to describe which pointer operations are safe and which lead to UB. People using the safe fragment of Rust won't care about this, but that's certainly not all of Rust.