The compiled code is also a lot slower. https://www.cis.upenn.edu/acg/softbound/
My point is that you can write your compiler spec to make explicit how exactly various kinds of UB are actually implemented, which then allows you to program to that spec and know that e.g. your overflowing bounds check is not completely eliminated from the program, but instead compiled into the machine instructions you had in mind.
If a compiler is verified to conform to such a specification, unintended changes in handling UB will be very obvious, since the spec will have to be changed to make the verification go through.
Yes, it does, because some optimizations now become invalid. For example, a compiler would no longer allowed to delete a provably out-of-bounds write. This happens all the time.
I don't think there's a lot of practical value in changing the definition of some kinds of undefined behavior to "memory corruption" (however defined) in the first place.