[saurik]

The type system proves things about my program that must be true and disallows invalid programs. The undefined behavior system decides things about my program that may or may not be true and just breaks my program when one of us is wrong (and I don't even care who: whether it is the compiler that came up with something insane or me trying to do the impossible <- I honestly don't care).

[erlehmann_]

I think when undefined behaviour is used for optimizations the programmer does not want it is more of a misunderstanding than one party (programmer or compiler) necessarily being “wrong”, as a compiler assumes that a program should make sense (i.e. is not undefined) and infers things from that. To clarify, would you say that assumption is problematic?