[angry_octet]

Well, it does define a subset of C... Anything in that subset will run as specified in a correct physical machine. So I don't get your point? Are you saying that a verified compiler is useless if you write buggy software? Because that isn't really a criticism.

Have you read anything about CompCert C or Coq?

[110011]

What OP is saying is if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct. And this does account for the vast majority of bugs (programmer error compared to compiler error).

[catnaroek]

> if you invoke undefined behavior in your program (like the Heartbleed bug for example) it doesn't matter that in the end the compiler is correct.

This is not true. It means that you can safely omit the compiler writer from the list of people to burn at the stake.

[kazinator]

> 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."

[catnaroek]

> Not if the problem is due to a compiler change which breaks something that has worked for decades and in other compilers too.

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.

[dhekir]

To complement: Leroy recently worked on a research project, Verasco, to formally verify a static analyzer for C (in the likes of Astree, Frama-C, Polyspace, etc.) that could plug that hole: if the analyzer reports "no undefined behaviors", then you are sure your program compiled with CompCert will result in a bug-free program. Turns out that it is very hard to scale such analyses, but with more research they may end up working for real-world programs.

[kazinator]

> then you are sure your program compiled with CompCert will result in a bug-free program.

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.

[angry_octet]

That is a super pedantic nit picking response. You well knew what was meant. Everyone here knows the meaning of V&V.

[kazinator]

Problem is, some undefined behaviors are actually correct. Some are documented extensions (a concept straight out of ISO C), and some are just nonportable situations that empirically work.

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.

[Blaisorblade0]

But you are aware real-world compilers are exploiting more and more UB and keep breaking existing software? Maybe you are, but the comment does not seem to reflect that.

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.

[kazinator]

> * Are you saying that a verified compiler is useless if you write buggy software?*

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.

[angry_octet]

Well, if I was writing something which had really serious failure consequences (space, aviation, crypto, bitcoin wallets, nuclear systems, etc) I think I would go to great lengths to minimise the unnecessary complexity, remove entire bug classes, etc.

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'.