I don't think it's that hard to reason about. Checking for overflow (and pointer-out-of-object-bounds, which is a special case of overflow) in C is like defusi

I don't think it's that hard to reason about. Checking for overflow (and pointer-out-of-object-bounds, which is a special case of overflow) in C is like defusing a bomb: you can't cut the red wire and then see if it exploded, you have to check that it won't explode before you cut the wire.