6 ms·

That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. For a bridge, you specify that

That's a pretty cynical take. I think a more profound problem is that formal specifications for software are fairly intractable. For a bridge, you specify that it needs to withstand specific static and dynamic loads, plus several other things like that. Once you have the a handful of formulas sorted out, you can design thousands of bridges the same way; most of the implementation details, such as which color they paint it, don't matter much. I'm not talking out of my butt: I had a car bridge built and still have all the engineering plans. There's a lot of knowledge that goes into making them, but the resulting specification is surprisingly small. Now try to formally specify a browser. The complexity of the specification will probably rival the complexity of implementation itself. You can break it into small state machines and work with that, but if you prove the correctness of 10,000 state machines, what did you actually prove about the big picture? If you want to eliminate security issues, what does it even mean that a browser is secure? It runs code from the internet. It reads and writes files. I talks directly to hardware. We have some intuitive sense of what it's supposed and not supposed to do, but now write this down as math...

pydry 3y ago
My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too. I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.
- AnimalMuppet 3y ago
  First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
  - NovemberWhiskey 3y ago
    >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
    - pfdietz 3y ago
      Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
      - NovemberWhiskey 3y ago
        Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. It's great at giving you counterexamples, so fuzzing is great for discovering vulnerabilities, but unless you're fuzzing your program's entire state-space (which is absolutely impossible for even relatively small programs) then you're not comparing like with like.
        pfdietz 3y ago
        So? The paper compared formal techniques vs. testing. Why is that suddenly not appropriate if the testing is fuzzing?
jackcviers3 3y ago
Browsers have been grown, not designed. The competitive pressures exuded on browsers to render ill-specified things and hacks has resulted in something essentially where what it does is what it does. That's the case with a lot of software,because we made the choice as a community of programmers to not formally verify the things that we build. Thunk of the origin of the blink tag [1]. We decided to be hackers, and doers, not thinkers. Just as testing changes the way you structure your software, designing via formal methods changes the code that you produce as well, and it will attract a different set of people than traditional software dev, just as architecture attracts a different set of people than carpentry. 1. https://danq.me/2020/11/11/blink-and-marquee/#:~:text=Invention%20of%20the%20element,being%20joining%20Netscape%20in%201994 https://danq.me/2020/11/11/blink-and-marquee/#:~:text=Invent....
zozbot234 3y ago
Type systems are "formal specifications for software" if perhaps in a fairly lightweight sense, and they work quite well. If you write a web browser in a strongly checked language such as Rust (the Servo folks are working on this, and shipping parts of their work in Firefox) you can ensure that it's not going to break memory safety, which is a start.
fwip 3y ago
A browser is possibly the most difficult application to formally specify. 99.somemorenines% of software has less complex specifications. The formal specification for something like Redis is likely much more akin to your car bridge spec. And to continue your analogy, I imagine the specifications for big bridges (Golden Gate, etc) are much more thorough than the ones you built.
- quatrefoil 3y ago
  A browser is one of the most consequential attack surfaces in the lives of billions of people. Redis isn't. Having proofs where said proofs don't matter much in the first place is not a particularly good use of our time. And FWIW, the correctness specs for Redis would be pretty intractable too.

pydry 3y ago

My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too. I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.

AnimalMuppet 3y ago
First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
- NovemberWhiskey 3y ago
  >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
  - pfdietz 3y ago
    Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
    - NovemberWhiskey 3y ago
      Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. It's great at giving you counterexamples, so fuzzing is great for discovering vulnerabilities, but unless you're fuzzing your program's entire state-space (which is absolutely impossible for even relatively small programs) then you're not comparing like with like.
      - pfdietz 3y ago
        So? The paper compared formal techniques vs. testing. Why is that suddenly not appropriate if the testing is fuzzing?

jackcviers3 3y ago

Browsers have been grown, not designed. The competitive pressures exuded on browsers to render ill-specified things and hacks has resulted in something essentially where what it does is what it does. That's the case with a lot of software,because we made the choice as a community of programmers to not formally verify the things that we build. Thunk of the origin of the blink tag [1]. We decided to be hackers, and doers, not thinkers. Just as testing changes the way you structure your software, designing via formal methods changes the code that you produce as well, and it will attract a different set of people than traditional software dev, just as architecture attracts a different set of people than carpentry. 1. https://danq.me/2020/11/11/blink-and-marquee/#:~:text=Invention%20of%20the%20element,being%20joining%20Netscape%20in%201994 https://danq.me/2020/11/11/blink-and-marquee/#:~:text=Invent....

zozbot234 3y ago

Type systems are "formal specifications for software" if perhaps in a fairly lightweight sense, and they work quite well. If you write a web browser in a strongly checked language such as Rust (the Servo folks are working on this, and shipping parts of their work in Firefox) you can ensure that it's not going to break memory safety, which is a start.

fwip 3y ago

A browser is possibly the most difficult application to formally specify. 99.somemorenines% of software has less complex specifications. The formal specification for something like Redis is likely much more akin to your car bridge spec. And to continue your analogy, I imagine the specifications for big bridges (Golden Gate, etc) are much more thorough than the ones you built.

quatrefoil 3y ago
A browser is one of the most consequential attack surfaces in the lives of billions of people. Redis isn't. Having proofs where said proofs don't matter much in the first place is not a particularly good use of our time. And FWIW, the correctness specs for Redis would be pretty intractable too.