Hacker News Reader

Comment by bluGill | Hacker News Reader

Formal methods catch a different class of problem from other tests and so are worth it. However they cannot catch everything. The classic example: "midpoint = (high + low) / 2" is easy to formally prove correct - but in fact it isn't correct because high + low could overflow.

View on HN

Any formal system worth its salt is going to model overflow.

And with SPARK/Ada it will. When I was learning it that was actually a very common thing that it caught in my code (various forms of over/underflow errors). In practice most of them would not occur, but a few could have under real-world use-cases.

There is a point here: if your implementation doesn't match the specification, then that can be the case. And your example presumes the specification assumed unbounded numbers, while an implementation did not have them. Well, in that case the specification just needs to be revised to include that information.

But the trick is to remember making the specification model the real world at sufficient detail: not too detailed to make the specification unwieldy, not too relaxed to skip real real-world issues that need to be modeled.

I don't think there are too many good solutions to that, except perhaps theorem provers from where you can also extract code from (e.g. Coq), but it seems either these tools are still difficult to use for engineers, or there is an expectation that models and actual implementations are going to be different anyway, making it difficult to see if the implementation actually implements the spec.

If you've formally proved that correct, then either it can't overflow or there's a massive bug in the prover.

I don't mean to be rude, but why are you commenting on formal methods when you clearly have no idea what they are?

The specific example I gave was from a 1982 paper (I forget who wrote it, but a big name in computer science) where that was used to prove an algorithm and thus argue that he didn't need to test it as it was proved correct.

The famous Donald Knuth has also stated "Beware of bugs in the above code; I have only proved it correct, not tried it.", which again hints that there are limits to proved programs.

I'll admit that I don't know much about them, what I know meringues me - but I can't figure out how to use them in the real world. However I know enough to know that they are not perfect.

You use them judiciously, you learn their capabilities and limitations and the scope of their applicability.

TLA+ is very useful, but it's not going to prove out your software itself, that will require testing or other methods, it will help prove out your specification. I've used it to good effect both for designing distributed and concurrent systems and for identifying issues in existing systems (without an existing formal spec, by creating it and then playing with the invariants and other aspects of the TLA+ spec). SPARK/Ada, I mentioned in my other comment, will detect many problems, and help you prove the absence of many others. But it's also not suitable (yet) for all projects, or more than a subset of a project, since it has specific limitations on what it can prove and is only compatible with a subset of Ada (this is being expanded each year). The subset of Ada it does apply to is actually quite significant and useful, but you have to be capable of understanding that it is limited and then apply it within that limited scope.

This is true for every other formal method approach I've seen. Pay attention, read, ask questions, and don't judge them all by one paper you half remember from 42 years ago.

Is "meringues me" a typo, or a really fun new vocab word for me?

Reply on news.ycombinator.com