The paper is fine but I took the quote that stood out from the article as the premise which made the conclusion seem odd to me. > Sorry, and again: how do you

The paper is fine but I took the quote that stood out from the article as the premise which made the conclusion seem odd to me. > Sorry, and again: how do you prove that the specification is correct? How do you prove that the proof is correct? By writing another proof of the proof? In practice it's not terribly useful to wring our hands around this issue. I'll leave that to the mathematicians. If you want to know if your specification is correct you either use a model checker to automatically check that some invariants hold over a universe of states or you use a theorem prover in which you trust the kernel. If you want to know whether you specified the correct properties, invariants, etc then you'll have to have someone review your work. With an interactive theorem prover at least some of this work can be done by the assistant but at the end of the day it's about thinking and testing your assumptions. > Absolutism is always wrong ;) Ha! Cute. I had thought the idea that formal verification will produce software free of all errors is well debunked these days. Maybe I'm wrong. I've always used to to prove only that certain properties hold. To prove the entire system is free of errors would be quite difficult and expensive indeed!