Testing a Formally Verified Compiler

Since there is often a misconception that formally verified software must be absolutely free from problems, from the conclusion of the paper: "Extensive testing on formally verified software is necessary for at least two reasons. First, the formal specification may not guarantee all the properties expected by users, but only critical ones (e.g. no miscompilation for CompCert). Second, critical bugs may still remain, because the formal specification might not exactly fit reality. However, in this case, critical bugs are in the—much smaller and simpler—[trusted computing base]"

Thanks for posting this, Dan! It's not usually the sort of thing that gets traction here but I found it a wonderful read, even starting just from the shock of the problem, “You spent all this time proving correctness and it's still not correct.”

Rich Hickey has a similar fun challenge in Simple Made Easy, he addresses the audience:

> A lot of people, as soon as they hear the words “reason about” [programs] they're like, “Oh my God, are you saying that you have to be able to prove programs?” I am not. I don't believe in that. I don't think that's an objective. I'm just talking about informal reasoning, the same kind of reasoning we use every day to decide what we're going to do. We do not take out category theory—we actually can reason without it, thank goodness. So what about the other side?

> There's two things you do with the future of your software. One is, you add new capabilities. The other thing is, you fix the ones you didn't get done so well. And I like to ask this question: What's true of every bug found in the field?

> “Someone wrote it—it got written?” — [eyeroll] Got written, yes, what's a more interesting fact about it?

> It passed the type checker! What else did it do? [Laughs, a couple things shouted]...It passed all the tests. Okay! So now what do you do?

> Right. I think we're in this world that I like to call guard-rail programming. It's really, really sad. We're like, "I can make change 'cause I have tests." Who does that? Who drives their car around banging against the guard-rails like “Whoa, I'm glad I've got these guard rails because I'd never make it to the show on time!” right? And—and do the guard rails help you get to where you want to go? Do they guide you places? No—there's guard rails everywhere, they don't point your car in any particular direction. So again, we're going to need to be able to think about our program, it's going to be critical, all of our guard rails will have failed us when we have a problem.

I really don’t understand how logophobic most programmers, even obviously very bright ones like Mr. Hickey, are.

I had an insight that only partially explains the phenomenon. American programmers, and of course Americans are the cultural standard for the supermajority of the programming world, are obsessively concerned with success in the marketplace. Even free software projects are prone to chasing users. And, as anyone can see, correctness is of virtually no importance to success in the marketplace. What determines commercial success is a different property called pleasantness. And thus it follows that we shouldn’t be surprised that most programmers have no use for rigorous logical reasoning.

There are of course those who enjoy making things unnecessarily complicated to revel in their own cleverness at being able to comprehend their complex creations, but I don’t find their existence to be sufficiently explanatory.

As an american programmer, I don't think you have it exactly correct (though I think you're getting close).

You're right that correctness isn't what I'm shooting for. Pleasantness is important only when the end user is also the one making the decision to use software (so roughly 0% of b2b sales), additionally pleasantness is only important once you've hit a certain floor on another metric, which is generally what I'm actually shooting for.

Usefulness is that metric. That is to say, the ability to use a piece of software to accomplish a practical task. This is, generally speaking, completely orthogonal to correctness, so long as the program is not so incorrect that it doesn't work at all.

The majority of my day is spent implementing business logic that has been decided by fiat by human beings and cannot be logically deduced. Additionally, it is subject to change by human fiat, and the new decision will be correct by definition, even if there are enough special cases that the truth table for the program may be as long as the actual program itself. This gronky business logic is where >80% of my bugs come from (assuming I'm working in a language that manages memory for me).

Proving things about the system doesn't seem particularly useful in that environment. Unless you can figure out how to prove that the VP of accounting is willing to accept a particular risk, or that a governance panel will sign off on a particular change. Political posturing in meetings and interviewing end users and teams working on parallel systems for undocumented requirements/changes my team wasn't told about offer higher ROI.

Americans also mostly don't study programming language theory (PLT) (unless they are lucky enough to attend e.g. Carnegie Mellon). A lot of the focus is on algorithms - which is a great shame. The majority of programmers will be consuming/creating APIs and abstractions, not implementing algorithms. PLT would be much more helpful here.