I think it's a major problem with our industry that so many programmers are amused by being technically correct.
Tradition notwithstanding, if a compiler deletes all my files because of the position of a comma in nested brackets, then I'm going to simply not use that compiler. I don't give a fuck if it's technically correct.
"Oh it's not a bug". Good for you. I don't care if you want to call it a feature or a bug. It's wrong. Press the issue and I'll find someone smarter.
It's true that I like to be technically correct. I don't consider this a problem itself. In fact, it can be quite important for programmers and mathematicians to be technically correct, as this bug in Cap'n Proto illustrates quite nicely.
However, this is not the only reason I'm pointing out that this is not a compiler bug. The other reason is that there are certain implications:
1. The compiler developers are likely to declare that this is not their problem.
2. The problem may exist for other compilers as well: even if it complies to the standard it may do this. Even worse, it may only show up in a new version of the compiler, or in specific situations.
I am not saying that this is a good situation and programmers should just be more careful. Everybody makes mistakes.
The root of the problem is at the specification. Ideally, there would be no undefined behavior. From an optimizer's point of view it is very sensible to assume that the programmer will not invoke undefined behavior and use optimizations based on this principle. People surely love a compiler which produces fast code, so it may not be desirable to totally eradicate undefined behavior (and end this kind of optimizations).
The most practical remedy I see is to add a debug flag which crashes or somehow indicates undefined behavior. Indeed, GCC has done this. So ultimately, we seem to agree that the compilers should change to improve this situation.
Agreed - I do not think the issue is with being technically correct, but in thinking that it always settles the matter and ends the discussion.
It would seem particularly unfortunate if a compiler were to do static analysis for undefined behavior, but only use it in optimization. From a cursory search, I found this blog post [1] explaining why LLVM does not warn about such things (at least in 2011, when it was written - attitudes may have changed, and the Clang project now has the UndefinedBehaviorSanitizer [2]). One of the arguments is that it is difficult to explain what the problem is, but in my view, that is an argument for making doing so a priority.
IMHO, more work should be done on proving properties of programs. If one could make a programming language like Dafny [1] less quirky but more developer-friendly, you can have programs which are both good-performing and proven to be consistent with their specification (but again, quirks in the specification may cause troubles).
Thanks for bringing Dafny to my attention. I agree with your first sentence, which is why I think it is a big deal that it can be a great deal harder, in practice, to reason about the behavior of a C program, if optimized, than the same program un-optimized. For one thing, unless you successfully reason about what the optimized code does when deploying an optimized build, then you are not deploying the program that you analyzed or inspected.
I think there is a sort of analogy with a large black hole here [1]: you can slip across the "event horizon" into undefined behavior without noticing, but, especially if you are using an optimizing compiler, there may be no escape.
[1] Maybe not, if the black-hole firewall hypothesis is correct.
It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
If I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.
Tradition notwithstanding, if a compiler deletes all my files because of the position of a comma in nested brackets, then I'm going to simply not use that compiler. I don't give a fuck if it's technically correct.
"Oh it's not a bug". Good for you. I don't care if you want to call it a feature or a bug. It's wrong. Press the issue and I'll find someone smarter.