Non-Argument Against Formal Methods

The cost/benefit tradeoff just can’t be solved for formal methods. There are far cheaper (in time, effort and financial cost) ways to write code with low enough incidences of bugs which are just more practical in almost all cases. Not to mention the fact that if you are manually implementing the code, someone can still just introduce bugs, and if you’re automatically generating the code, there can be bugs in that code generator, or if you’re using an automated verifier ther could be bugs in that. At some point a human had to write some code that can’t be proven to be “correct”.
Formal methods seem great for mathematicians and lousy for everyone who wants to make something productive in a reasonable time frame.

I call this a “goal post” argument and the argument strategy is about drawing an arbitrary boundary that something must be beyond to be valid. In this case the argument is about “trust” but if you break it down you notice it makes absolutely no sense. The author of that comment clearly “trusts” the hardware/CPU running their software. But, if they trust the hardware/CPU then they implicitly trust whatever process created the CPU and the process used to make the CPU was more people and software. So the whole argument collapses and they must trust the software. It’s circular reasoning in another guise.

What, Why, and How of Formal Methods


Now that I’m one of the organizer of the formal methods meetup it has become a bit more clear why most programmers are not familiar with the general landscape of formal methods. It’s mostly a lack of awareness about what is available out there so to help fill in the awareness gap this post is meant to serve as a brief introduction to some of the vocabulary and high level concepts of formal methods.

This post consists of 3 main sections. 1st is about the general concepts and high level classification(s) of formal methods. 2nd is about why we should care about formal methods in software engineering. 3rd is about concrete applications of formal methods and some pointers for how to apply them in day to day software engineering.

Continue reading