Formal Methods in computer science are well summarized in Wikipedia:
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based technique for the specification, development and verification of software and hardware systems.[1] The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
I’ve commented on a number of occasions, usually to colleagues, that some day the profession has to find a way to apply Formal Methods in order to produce better products, even if I haven’t the faintest idea of how to do it myself[1]. It’s good to see that some folks have been pursuing this objective, as noted in this pop-sci report on TLA+, which appears to be based on that notion:
TLA+, which stands for “Temporal Logic of Actions,” is similar in spirit to model-based design: It’s a language for writing down the requirements—TLA+ calls them “specifications”—of computer programs. These specifications can then be completely verified by a computer. That is, before you write any code, you write a concise outline of your program’s logic, along with the constraints you need it to satisfy (say, if you were programming an ATM, a constraint might be that you can never withdraw the same money twice from your checking account). TLA+ then exhaustively checks that your logic does, in fact, satisfy those constraints. If not, it will show you exactly how they could be violated. [Pocket / The Atlantic]
The title reminds me of a chapter in FUNCTIONAL PROGRAMMING: Theory and Practice (MacLennan), in which the passage of time had to be accounted for by the functional programmer. Apparently functional theory didn’t account for the passage of time, and the author found this to be a problem that had to be treated. I fear I missed the point of that chapter.
I must say, though, that one of the arguments the driving force behind TLA+, Leslie Lamport of Microsoft, employs falls with a thud to the ground:
For Lamport, a major reason today’s software is so full of bugs is that programmers jump straight into writing code. “Architects draw detailed plans before a brick is laid or a nail is hammered,” he wrote in an article. “But few programmers write even a rough sketch of what their programs will do before they start coding.” Programmers are drawn to the nitty-gritty of coding because code is what makes programs go; spending time on anything else can seem like a distraction. And there is a patient joy, a meditative kind of satisfaction, to be had from puzzling out the micro-mechanics of code.
The problem is that it’s a rare person who has the resources to build a skyscraper on a whim. Programming, though, all you need is the compiler for the language of choice, and a computer. Anyone with a little intellectual gumption – or gall – can sail right into writing a program. And once someone gets the taste of success in their mouth, it can take years to wash it out. The analogy is broken.
The ease of writing code tends to obliterate the importance of the entire enterprise, truth be told. I recall way back when I was just starting to write code, I ran across a guy – I can’t remember his name – who didn’t consider it science, nor engineering. For him, it was an art form. This is not to say that all software engineers go to that extreme, but given how easy it is to indulge in writing software – programs, apps, code – compared to building even a shack, it’s not surprising that there’s a lot of undisciplined writing of code out there, me included.
But code is written everyday for critical, life-involved applications. Forget “mission-critical,” I’m talking embedded software in medical devices, the software that controls various energy sources, all things that can cause death if they fail. The use of tools such as TLA+ should continue and grow, otherwise the promise of computers will be blighted.
But it’ll probably be after my time.
1 I know I’ve mentioned related topics on this blog, specifically having to do with software dis-warranties and the general use of the customer as a beta-release mechanism.
