So far all the comments have focused on this issue as a C language specific problem, as if some other language won't be affected, but it's really universal to optimizers. Optimization is subtle and hard. JIT engines get burned, too.
In any other case, the answer is almost certainly no. Most commonly used C compilers are sufficiently large and complicated that the chances of avoiding a compiler bug with a sufficiently large codebase is close to zero.
Thanks for the heads up, I hadn't seen anything in the article about CompCert, but on doing a search I found there are quite a few mentions of it on other articles on the blog:
They also created VCC (Verifying C Compiler), which uses their Z3 theorem prover to check for bugs (especially concurrency bugs, which can be really tough to find).
SAL and VCC are for making C programs correct. This is related but not the same thing as making the C compiler correct. These source-level tools assume that the compiler translates the programs correctly.
I realised that, as Pascal might put it Cyclone is a C like language designed to ensure that programs are correct. I saw it as a related form of safety others might be interested in.
I already posted on Clight & CompCert which is much more salient in terms of ensuring compiler correctness and a safe subset that falls within the scope of the verified compiler's correctness.
I used to work for a large defence company. They paid for "certified" ADA compilers for PPC architecture. They had as many (if not more) bugs. Not only that, they built their stuff on FPGAs which had even buggier compilers than the compilers for the software.
Certified compilers are protected only by maintenance agreements.
When a piece of software is verified with an Agda proof, that is generally a real proof. The proof may not cover all aspects, but in those aspects you really do not have bugs.
Perhaps you mean non-proven certification? Or a weak certification of too few aspects?
I think it was probably a weak certification in this case. They paid for core concerns to be covered, not necessarily the entire toolchain (which TBH is where the problems were - X working with Y properly). In fact I think it was that linker that fluffed stuff. I should modify my comment really.
Historically, compiler certification is a bad joke. It amounts to concerted testing at best, and wishful thinking in most cases. Few (remotely useful) compilers have been verified in any mathematical sense, and even then there is generally a wide gulf between what is proved and what we would intuitively expect a truly correct compiler to do.
