There is an interesting article about How Amazon web services uses formal methods.
I was quite surprised to learn that a major software vendor had enthusiastically embraced formal methods, and were using for major software developments.
The article offers the following highlights:
- Formal methods find bugs in system designs that cannot be found through any other techniques we know of.
- Formal methods are surprisingly feasible for mainstream software development and give good return on investment.
- At Amazon, formal methods are routinely applied to the design of complex real-world software, including public cloud services.
A precise, testable description of a system becomes a what-if tool for designs, analogous to how spreadsheets are a what-if tool for financial models.
Formal methods have helped us devise aggressive optimizations to complex algorithms without sacrificing quality.
Executive management actively encourages teams to write TLA+ specs for new features and other significant design changes.
I was first introduced to formal methods through the book, Error-free software: know-how and know-why of program correctness by Robert Laurence Baber back in the early 1990’s. I was taken by the simplicity of the idea, and seduced into believing that I could really prove the correctness of programs.
Buoyed by my enthusiasm, I used formal methods in two (2) projects at work:
- Design and implementation of a tape management for the AS/400
- Review of design for uptime calculation based on Net/Master logs
In the latter case, I converted a written description of the system into formal notation and proceeded to find various design flaws.
What dampened my enthusiasm for formal methods was that I had to check all proofs by hand. This was a very tedious, time-consuming, and error-prone process.
However, my work colleagues were less than impressed with my efforts in this area, and could not see any real benefit to formal methods. There appeared to be very little return on investment.
In 1996-7, as part of my master’s coursework in Computer Science, I did a subject on Formal Methods, and did a project in coming up with a formal description of an operating system. In the class on Formal Methods, I used the following text-books:
- “Programming from Specifications” by Carroll Morgan (1994), Prentice-Hall
- Communicating sequential processes
Both of these books went far beyond what Baber presented in his book. And there was still no automated proof engine available even as a research student at university. Needless to say that I did not get very far with my formal specification of an operating system. There was simply too much to be done through manual methods by a single student.
After university, I discovered the Z notation which standardised the approach to formal methods.
But when I started to get involved with databases, I was all at sea again as the books at the time did not address database design—they were still concerned with program design. Then along came Applied Mathematics for Database Professionals. This got me enthusiastic for a while, but I had not had any chance to apply the methodology at work.
My last engagement with with formal methods was with the logical design for Much Ado About Nothing. Since then, I have left formal methods in abeyance.
Maybe this article could get me interested in reading about TLA+.