> The problem with your interpretation is that it defies causality. The question of whether this is a well-formed C++ program isn't one that can be delayed until runtime, it either was, or was not, a well-formed C++ program when it was compiled - so if your reading requires that we don't know until runtime then it cannot be a correct reading.
Alas, the same issues with causality arise with the idea of "time-travelling UB". Suppose I write a program that prints a welcome message, reads a number from the standard input, then either exits if it's 0, or causes UB if it's 1. By the rules of the standard, if the implementation could presciently predict at the start of the program that I am about to enter 1, then it could skip the welcome message.
But of course, in the real world, causality is a higher law than the rules in the standard: if there's a possibility at any point that UB might not occur, then it must keep functioning as expected. So there's no way it can skip the welcome message, even though the standard allows it.
I see the question of ill-formedness from invalid terms as the same. At the start of each execution of the program, each type that must satisfy a requirement gets an invisible "set of valid terms" with respect to that requirement. However, this set exists only in the mathematical sense, in that it cannot yet be known by anyone, since it depends on future information. This is just like "the number that I will eventually enter" in my last example: it mathematically has some value (assuming that I do eventually enter something), but neither I nor the implementation can know whether it's 0 or 1 until I actually enter it.
Thus, the implementation is once again bound by the possibility that the "set of valid terms" might truly satisfy the requirement. It must execute the program as if it is well-formed, right up until the point where it is no longer possible that it is well-formed. And that point will generally correspond to a particular witness value (e.g., a NaN) that is passed into a standard function but makes an operation fail to meet its requirements.
If you want to put it into properly-causal terms, you could start the program with a really big "set of possible sets of valid terms". Then, each time at runtime that the program passes a value to a function with the requirement, you filter the sets to only those containing the value. If there are no sets left after this, then the program is now known for certain to have been ill-formed all along (there's no possibility remaining), so you can do whatever you want.
Of course, this does assume that a program being well-formed can change between each execution, even with the same source file. But it's hardly the only IFNDR in the standard that depends on behavior rather than syntax.
> The other option (which I happen to think is the only reasonable choice) is the one Rust took - only programs which we can show have the desired semantic properties will compile, other programs are rejected. This means the compiler will reject some correct programs, which is somewhat annoying if it happens to you, but effort put into the compiler can reduce the frequency of its occurrence (and it did in Rust, that's what the Non-Lexical Lifetimes change was and what Polonius is all about)
Since you mention Rust, I'd note that it has the same causality wackiness, just to a far lesser extent than C/C++, in the form of "angelic nondeterminism" (which is a term you can Google). Suppose that you have a pointer to the end of one slice and a pointer to the start of another slice, which happen to be equal, but don't have access to each other's slices due to provenance. Then, you convert both those pointers to integers, and convert that integer value back to a pointer.
Which slice should the new pointer have access to? Since integers have no provenance, the compiler has no way of knowing which pointer the address came from! Thus, the compiler uses "angelic nondeterminism" to decide: defying causality, it picks whichever of the two slices will make the program valid. If neither choice is valid (e.g., the program tries to access both slices from the new pointer), then it's instant UB.
Once again, to do this in the real world, the compiler must maintain a conceptual set of possible pointers that the new pointer might have come from, then whittle them down based on what memory is actually accessed. If there are no possible pointers left, then UB is known.