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.

https://bit.ly/2Wkuz55

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.