Re:Formal Verification Creates Hacker-Proof Code (2016)
by pron on Friday May 01, 2020 @07:28PM
(#23047564)
1. TLA+ doesn't "find" or not find anything. It is a mathematical language for describing systems and assertions about them. There is a proof assistant for TLA+ that checks your formal proofs of theorems that say that your assertions follow from the description, and model checkers that verify your theorems automatically.
2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description.
3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.
2. If you use the model checker, it's not about it "failing to find" a counter example. A model checker result is a proof that no such example exists. True, it is usually a proof about some finite instance of your system description.
3. There is just no such thing as proving a system flawless. Software systems are physical systems exhibiting probabilistic behaviors. At best you can prove things about a mathematical description of a system, which mean that as long as the physical system behaves according to the description, the result follows. Of course, the first part at best holds with some probability.