Does it? It's very unclear to me whether something like type punning is prohibited by provenance today. The docs don't provide much clarity, and the comments I can find by ralf suggest the details are undecided. I can't imagine it won't be eventually prohibited since we already have hardware designs prohibiting it and it's a terrible code pattern to begin with, but I don't know if the language currently does so.

This isn’t correct. Just because Rust has aliasing rules doesn’t mean they’re the same sorts of rules.

C and C++ are also looking to adopt more formal provenance rules.