[Someone]

So, how much effort should the standard require a compiler to make for “if and when you can prove it”? You can’t, for example, reasonably require a compiler to know whether Fermat’s theorem is true if that’s needed to prove it.

There are languages that specify what a compiler has to do (e.g. Java w.r.t. “definite assignment” (https://docs.oracle.com/javase/specs/jls/se9/html/jls-16.htm...)), and thus require compilers to reject some programs that otherwise would be valid and run without any issues, but C chose to not do that, so compilers are free to not do anything there.

[vintermann]

Everyone wants to drag nontermination into this, but in the OP's example, the compiler already had proof that a the conditional would never evaluate to true. What you can or can't prove in the bigger picture isn't so interesting when we already have the proof we need right now.

It's just that it used this proof to remove the conditional evaluation (and the branch) instead of warning the user that he was making a nonsensical if statement.

So to the question of "when can we hope to do it" the answer is, "not in all cases, sure, but certainly in this case".