Author here. While you are technically correct, the key is your own statement: > where it mostly suffers existentially. Yes, theorem provers exist, and they

Author here. While you are technically correct, the key is your own statement: > where it mostly suffers existentially. Yes, theorem provers exist, and they work. But proving that the end result, the actual machine code, corresponds to the proven code, is the big problem. When I talk about correctness in the post, I'm really referring to two things: 1. Correctness as you have defined it, 2. The compiler artifact being as faithful as possible to the input source code. Avoiding UB is an excellent way to improve the latter.