Testing a Formally Verified Compiler
Thanks for posting this, Dan! It&#x27;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&#x27;s still not correct.”<p>Rich Hickey has a similar fun challenge in <i>Simple Made Easy</i>, he addresses the audience:<p>&gt; A lot  of people, as soon as they hear the words “reason about” [programs] they&#x27;re like, “Oh my God, are you saying  that you have to be able to <i>prove</i> programs?” I am not. I don&#x27;t believe in that. I don&#x27;t think that&#x27;s an objective. I&#x27;m just talking about informal reasoning, the same kind of reasoning we use every day to decide what we&#x27;re going to do. We do not take out category theory—we actually <i>can</i> reason without it, thank goodness. So what about the other side?<p>&gt; There&#x27;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&#x27;t get done so well. And I like to ask this question: <i>What&#x27;s true of every bug found in the field?</i><p>&gt; “Someone wrote it—it got written?” — [eyeroll] Got written, yes, what&#x27;s a more interesting fact about it?<p>&gt; 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?<p>&gt; Right. I think we&#x27;re in this world that I like to call guard-rail programming. It&#x27;s really, really sad. We&#x27;re like, &quot;I can make change &#x27;cause I have tests.&quot; <i>Who does that?</i> Who drives their car around banging against the guard-rails like “Whoa, I&#x27;m glad I&#x27;ve got these guard rails because I&#x27;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&#x27;s guard rails everywhere, they don&#x27;t point your car in any particular direction. So again, we&#x27;re going to need to be able to think about our program, it&#x27;s going to be critical, all of our guard rails will have failed us when we have a problem.