Informal reasoning works well on a small scale but is inadequate for understanding large, complex systems. Informal reasoning is especially inadequate when handing decisions over to machines. For example, one of the things you’d like to program an automated car to do is obey traffic laws. But is it even possible to obey all traffic laws? Surely there are inconsistencies in traffic laws that humans can gloss over using common sense but that could stymie a computer.
Formal methods
Formal methods lets us reason about systems that are too complex to completely understand intuitively. These methods produce machine-verified mathematical proofs of properties of a system. This high degree of assurance is not necessary for systems that can afford to fail occasionally. But when the consequences of failure are high, formal methods are worth the effort. Critical software, such as that controlling health and safety equipment, or security, or large financial transactions, needs to be correct, and formal methods help achieve that goal.
Formal methods help you explore corner cases, combinations of conditions that are unlikely to be tested. Large systems with many users inevitably run into such corner cases. This is why Amazon Web Services, for example, has required formal validation with tools such as TLA+ for several years now. (See this report for details.)
Synergy with traditional methods
Even when complete formal validation is not practical, any degree of formal validation is complementary to traditional forms of testing. Formal methods and execution testing catch different kinds of errors. You can have more confidence in a system that passes traditional testing and formal verification than a system that passes either alone.
There is a spectrum of formal methods, starting with strongly typed, pure functional programming languages like Haskell to full-fledged interactive theorem provers like Coq. The level of formality can adjust to the context of the problem at hand.
Applications
If you have a complex set of procedures, would you like to know whether these procedures leave anything out? Whether they contain any ambiguities or contradictions? Whether a proposed change is consistent with existing procedures? This is a task well-suited to testing with formal methods.
When you are designing a complex system, one requiring input from many people, you may work hard only to achieve the illusion of consensus. Different parties may think they agree when they have not been explicit enough to realize that they disagree. These kinds of misunderstandings become more expensive to resolve the longer they take to surface. Formal methods can save money by helping groups come to a genuine consensus earlier.
If you’d like to discuss how formal methods can benefit your project, and how to implement them, please call or email to discuss your project.