7 ms·

Testing a Formally Verified Compiler

129 points by luu 3y ago

mafribe 3y ago
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]"
- DonaldPShimoda 3y ago
  An excellent clarification to make. "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. Bugs can exist in three places, then: 1. Within the theorem-proving software. 2. Within the proposition itself. 3. Within the portions of the code that are not formally verified. We generally have good reason to suspect bugs in (1) are almost nonexistent. Bugs in (2) and (3) are relatively common, but (3) is no different from the bugs present in software with no formal verification. A lot of modern theorem-proving research lies in helping people to address bugs in (2) by making propositions easier to write and verify, and in (3) through the same mechanism (because then we can formally verify a greater portion of the software).
  - astrange 3y ago
    > "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).
    - wtroughton 3y ago
      A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) ) Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?
    - DonaldPShimoda 3y ago
      I know what you're saying, but there's a difference between "the expected behavior has been rendered as a proposition" (what I said) and "the expected behavior corresponds with a proposition" (what you're saying). To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.
crdrost 3y ago
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.
- User23 3y ago
  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.
thanatos519 3y ago
Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth
- red75prime 3y ago
  I'd be content if the compiler was also written by Knuth and the processor was designed by Knuth and physical laws was created by Knuth.
  - taeric 3y ago
    Oddly, he wouldn't. He very much appreciates exploring the work of others. Such that large portions of his writing is historical in nature.
eru 3y ago
> Source semantics mismatch: the C language is surprisingly complicated, and its semantics as formally defined in CompCert may diverge from the informal one defined in the standard, or in CompCert’s manual. That's quite the understatement.
dorianh 3y ago
If I understand correctly, the authors feared that C-Reduce could introduce undefined behaviors: > Unfortunately, if given the opportunity by a lax predicate, C-Reduce will write programs that have undefined behavior I don't think this is true, in the introduction of [1]: > Our reducers do this automatically and without introducing undefined behavior into the reduced test cases [1] https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf

129 points by luu 3y ago

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

DonaldPShimoda 3y ago
An excellent clarification to make. "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. Bugs can exist in three places, then: 1. Within the theorem-proving software. 2. Within the proposition itself. 3. Within the portions of the code that are not formally verified. We generally have good reason to suspect bugs in (1) are almost nonexistent. Bugs in (2) and (3) are relatively common, but (3) is no different from the bugs present in software with no formal verification. A lot of modern theorem-proving research lies in helping people to address bugs in (2) by making propositions easier to write and verify, and in (3) through the same mechanism (because then we can formally verify a greater portion of the software).
- astrange 3y ago
  > "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).
  - wtroughton 3y ago
    A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) ) Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?
  - DonaldPShimoda 3y ago
    I know what you're saying, but there's a difference between "the expected behavior has been rendered as a proposition" (what I said) and "the expected behavior corresponds with a proposition" (what you're saying). To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.

crdrost 3y ago

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.

User23 3y ago
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.

thanatos519 3y ago

Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth

red75prime 3y ago
I'd be content if the compiler was also written by Knuth and the processor was designed by Knuth and physical laws was created by Knuth.
- taeric 3y ago
  Oddly, he wouldn't. He very much appreciates exploring the work of others. Such that large portions of his writing is historical in nature.

eru 3y ago

> Source semantics mismatch: the C language is surprisingly complicated, and its semantics as formally defined in CompCert may diverge from the informal one defined in the standard, or in CompCert’s manual. That's quite the understatement.

dorianh 3y ago

If I understand correctly, the authors feared that C-Reduce could introduce undefined behaviors: > Unfortunately, if given the opportunity by a lax predicate, C-Reduce will write programs that have undefined behavior I don't think this is true, in the introduction of [1]: > Our reducers do this automatically and without introducing undefined behavior into the reduced test cases [1] https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf