> And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on

> And actually as usual Rust is ahead of the game here, you say "the compiler has no way of knowing" - actually with Aria's experiment in play we can insist on always telling the compiler what's going on, and as a reward we get both more assurance of correctness because the tools work (Miri for example) and better performance. The experiment is about whether most Rust software can live with this restriction ("Strict Provenance") and the answer IMNSHO is clearly yes. The standard counterexamples being XOR linked lists, or manual paging with mmap, or manipulating addresses as integers within asm!(), or literally any situation where you can't afford to keep the address as a single value-with-provenance sitting at a known location in program memory until you need it. Strict provenance is sufficient for most use cases, but far from all of them, so there's no viable way to tear the whole concept of exposed addresses out of the language. In any case, removing it would violate basic expectations of stability, given that users have been converting pointers to integers and back since the very beginning of the language. > More pertinently to our discussion, even with PNVI-ae-udi plus a mistake that results in an impossible pointer this is a cause of Undefined Behaviour, which occurs at runtime, it is not a semantic requirement of the language, our Rust program was well formed and correctly translated into machine code if we did this wrong, it's just that it had Undefined Behaviour at runtime as a result of us writing bad unsafe code. My point is that there's no difference in semantics, nor any difference with respect to causality, between an "ill-formed program" that's only ill-formed under certain conditions, and a program with "Undefined Behavior at runtime". The standard ascribes no requirements on the entire execution, start to finish, in either case. But practically, if the implementation doesn't have enough information to distinguish a valid execution from an invalid execution until a certain point (i.e., runtime-dependent UB or ill-formedness), then it must behave properly right up until that point, by the laws of causality. Still, I agree that just calling requirement violations UB would be far less confusing.