I remember hearing in class once that formal methods are mostly used to catch bugs. But tools like Coq seem capable to do more than that. So how is it that they are used to catch bugs if they are mostly used for proofs (i.e. showing statements provably work)?
Why are proof assistants used mostly to catch bugs instead of using it to truly proving correctness?
It’s hard to be sure what your professors meant, but formal methods include much more than proof assistants — for instance, they include model checkers, which aren’t so different from QuickCheck & friends, which are indeed testing tools.
And strictly speaking, “formal methods” include type systems, which are certainly a tool to catch (and sometimes rule out) certain classes of bugs.
I think the statement is out of date. And vague (“mostly used” by whom, for what purpose, etc.).
1 Like
If you try to convince industry deciders to invest in the usage of a proof assistant, using the leitmotiv that they are good at catching bugs may be a strong argument. I used this argument just a few days ago in a course, where the target audience was software engineers.
Very few practical real-world systems can be fully verified by tools, let alone proof assistants. One important reason is that simply specifying a system end-to-end in a reasonable way is very demanding.
However, many systems have “core components” which can be specified in isolation, and thus verified at the implementation level. One typical example is the consensus protocol of a blockchain system (distributed transaction ledger). As shown in this paper, having verified core components means that system faults can be traced to bugs in fewer places than otherwise, such as the interface between verified and external/unverified code, and unverified components. I argue this is not about “catching” bugs, but about ruling out that errors occur due to core component behavior - which means overall testing effort and debugging time decreases.
1 Like