Comment by pron

3 days ago

But both Dafny and Lean (which are really hard to put in the same category [1]) are used even less than TLA+, and the problem of formally tying a spec to code exists only when you specify at a level that's much higher than the code, which is what you want most of the time because that's where you get the most bang for you buck. It's a little like saying that the resistance to blueprints is that a rolled blueprint makes a poor hammer.

TLA+ is for when you have a 1MLOC database written in Java or a 100KLOC GC written in C++ and you want to make sure your design doesn't lead to lost data or to memory corruption/leak (or for some easier things, too). You certainly can't do that with Dafny, and while I guess you could do it in Lean (if you're masochistic and have months to spare), it wouldn't be in a way that's verifiably tied to the code.

There is no tool that actually formally ties spec to code in any affordable way and at real software scale, and I think the reason people say they want what doesn't exist is precisely because they want to avoid the thinking that they'll have to do eventually anyway.

[1]: Lean and TLA+ are sort-of similar, but Dafny is something else altogether.

7 comments

pron

Reply
sirwhinesalot  3 days ago

Architectural blueprints are very precise. What gets built is a more detailed form of what is in the blueprint.

That is not the case for the TLA+ spec and your 1MLOC Java Database. You hope with fingers crossed that you've implemented the design, but have you?

I can measure that a physical wall has the same dimensions as specified in the blueprint. How do I know my program follows the TLA+ spec?

I'm not being facetious, I think this is a huge issue. While Dafny might not be the answer we should strive to find a good way to do refinement.

And the thing is, we can do it for hardware! Software should actually be easier, not harder. But software is too much of a wild west.

That problem needs to be solved first.

  • pron  3 days ago

    > That is not the case for the TLA+ spec and your 1MLOC Java Database.

    That is the case. Of course, nobody bothers to write the TLA+ proof that that is the case, because even if somebody had the resources to do it, the ROI on doing that is not good. If you can avoid 4 major bugs with 10 hours of work, you probably won't want to work an extra 10,000 hours to avoid two additional minor ones. That most people choose to stop when the ROI gets bad and not when they achieve perfection is not a problem.

    The question isn't what tool guarantees perfection (there isn't one), but what toolset can reduce the greatest number of (costly) bugs with the least effort, and tools that help you think rigorously about design are a part of such a toolset.

    > You hope with fingers crossed that you've implemented the design, but have you?

    The same way you always validate that you've implemented what you intended - which is more than just keeping your fingers crossed - except that TLA+'s job is to make sure that what you intend actually works (if implemented).

    > While Dafny might not be the answer we should strive to find a good way to do refinement.

    TLA+ does refinement in a much more powerful way than Dafny. Neither is able to do it from a high-level design to a large and realistic codebase, certainly in any afforable way, but nothing can. I guess that is a problem, but it's not the problem we can solve, and there are other big problems that we can.

    • sirwhinesalot  3 days ago

      Too defeatist. If much of the software infrastructure of the world was built on say... Idris, we could do it. That's the promise of dependent types, proof carrying code.

      Can we extend that to large scale software? There's no obvious barrier to it, beyond a lack of existing provably correct code to build upon.

      I don't expect this to change, however, since the cost/benefit ratio just isn't there. And that makes me sad. We build everything on quicksand.

      1 reply →

pjmlp  3 days ago

Appreciation isn't the same as market share, formal proofs in general are pretty much inexistent in enterprise, unless there are legal requirements to do otherwise.

I fail to see how you validate that TLA+ model is actually correctly mapped into the written Java code.

  • pron  3 days ago

    > formal proofs in general are pretty much inexistent in enterprise, unless there are legal requirements to do otherwise.

    Formal proofs are rarely used when specifying with TLA+, too, BTW. Writing formal proofs (as you would in Lean) has a very low ROI, and even formal method fans (like me) would tell you that's a tool you should reach for very rarely, and only if you must.

    > I fail to see how you validate that TLA+ model is actually correctly mapped into the written Java code.

    You don't (not even with Lean), but that we can't have cars that are completely crash-proof doesn't mean that's the standard for accepting or rejecting a safety measure. With TLA+ you can make sure that the design that you have (and you can't validate is actually implemented in code with or without TLA+) is actually good.

    In other words, it lets us think about design rigorously. Maybe that's not all we wish for, but it's a lot, and it's not like there are better, easier ways of doing that. Of course, if the goal is to avoid thinking hard about design, then a tool that helps us think even harder isn't what we want.