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 6 days ago | parent [-]

> 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 6 days ago | parent [-]

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.

	▲	pron 6 days ago \| parent [-]
		> There's no obvious barrier to it It's like saying that there's no barrier to turning lead into gold except for the fact that it's easier to get gold by other means; that's a good thing! The cost of deriving formal deductive proofs is high, while unsound methods are much cheaper and highly effective. The reason proofs can be expensive is that proving things has an intrinsic computational complexity cost (it's a search problem in a large space). A decade ago I summarised some relevant results of the last three or four decades about the difficulty in proving programs correct: https://pron.github.io/posts/correctness-and-complexity If software were generally simple enough for all of its interesting properties to be easily proven, that would mean that there wouldn't be much point in the software at all. I think it was a formal methods researcher/practitioner at NASA who once said something like, "computers were built to surprise us; if they didn't, there would be no point in building them in the first place." > We build everything on quicksand. You do realise that while an abstract algorithm or a program on the page can be proven correct, it is impossible to prove that a software system is correct, because it's a physical system, and not a mathematical object anymore (you cannot prove that hardware will behave as specified). If mathematical proofs were the only thing that's not "quicksand", then everything in the physical world is quicksand.