I think that only works if your language traps underflow. In a language like C++ where unsigned integers silently wrap around, you’re not really ensuring that y

I think that only works if your language traps underflow. In a language like C++ where unsigned integers silently wrap around, you’re not really ensuring that you cannot represent invalid values, merely that you represent invalid values as valid values.