Have you read anything about CompCert C or Coq?
This is not true. It means that you can safely omit the compiler writer from the list of people to burn at the stake.
Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too.
Say we have an open source distro full of programs, and a compiler change breaks some program that hasn't been touched in years so that it misbehaves in situations where old builds of that program do not.
This means the compiler writers aren't testing with a full distro, and possibly that they don't care.
"We can do anything we want within the limits set out by the ISO language spec, and that spec alone; let the downstream consumers sort out whatever happens."
The compiler writer is within their rights to perform any changes that don't contravene the language specification, whether it breaks other people's code or not.
> "We can do anything we want within the limits set out by the ISO language spec, and that spec alone; (...)"
Yes.
> "(...) let the downstream consumers sort out whatever happens."
It's the language user's responsibility to make sure they write meaningful programs.
These could be handled in the prover; you just need an extended language definition. Or maybe not. Depending on what is being relied upon, it could be difficult.
In any case, a prover based on equating "correct" with "strictly conforming ISO C" is going to be of severely limited use. It might be good for some module-level assurance, like that some linked list or hash table module is perfect or whatever.
Either way: The good thing is, after compiler writers start exploiting a kind of UB they add options like `-fno-strict-aliasing` and pinky swear that option preserves the UB. I agree a useful checker should support real-world relevant C dialects.
That is simply not true. A UB-free program which calculates e is incorrect, if the task was to calculate pi. Anything downstream from that program which uses its output as if it were pi is going to break.
Correctness is only with respect to a specification.
Specifications can have issues. Aside from being vague or contradictory, they can neglect to include important requirements, such as being completely silent on the treatment of bad inputs. A program with an exploitable security flaw outside of its intended operation can in fact be correct, because those inputs lie outside of its requirements: i.e. just like a compiler, the program has its own undefined behaviors. Also, the requirements for a program can explicitly call for undefined behavior, like "divide a number by zero to demonstrate/test the platform-specific handling of the situation".
Calling a function outside of ISO C that is not defined in the C program itself is also undefined behavior, so these proven programs cannot use any platform libraries without relaxing what "undefined behavior" means.
Not exactly, but if we look at it that way, how is it wrong?
I write buggy software; what do you write?
With the approach I take to writing software, the methods by which I flush out my bugs find compiler issues also in the same stroke.
If I didn't write buggy software, I could ditch testing, right?
Except, oops, not without a proven toolchain.
Now, a compiler is not a simple thing, and one which does optimisation steps is doing something complicated to code one may already by reasoning about in complicated ways.
I've encountered a number of compiler bugs, but usually in the sense of it crashing or doing something violently wrong. I've never encountered one in terms of it doing something very subtly wrong, but I consider it likely that that could be going on, but that I have no way to test for it. The only way would be to have dual implementations producing matching output, and it would still be dependent on the test vectors, and even then it could be a common mode error. So, for me, it would be very useful to be able to remove the compiler from the list of possibly buggy components. In fact you could say that this is the first C compiler ever, the others compilers have been for some close cousin of C.
So, I don't really thing your argument holds. Testing is notoriously hard to get right, and testing which simultaneously accounts for complex compiler interactions seems implausible. Especially compared to 'use a verified compiler and stop worrying if the compiler got it wrong'.