[abjKT26nO8]

> Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive.

Most code doesn't check whether incrementing a variable causes an overflow, so in practice the test you're referring to is still vulnerable.

[anyfoo]

No, because when you are formally verifying programs, or employing a type system that implicitly does so, you take that overflow and any other "surprising" behavior into account. Verifying that the program either cannot reach such an overflow condition, or otherwise handles it correctly, is exactly the point of formal verification.

It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.)

I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.