[SystemSafety] Bursting the anti formal methods bubble

[C. Michael Holloway]

Almost certainly I will regret participating in this thread, but here 
goes anyway. ...

I'm not making an argument, but simply recounting two bits of history. 
Some of you may remember one or both of them. Some of you may not be 
aware of either.

A little more than 21 years ago, /IEEE Computer/ (Volume: 29, Issue: 4, 
April 1996) ran a 16 page collection of 'roundtable' articles under the 
title "An Invitation to Formal Methods". Contributors included Jonathan 
Bowen, David Dill, Robert Glass, David Gries, Anthony Hall, Michael 
Hinchey, Daniel Jackson, Cliff Jones, Michael Lutz, David Parnas, John 
Rushby, Jeannette Wing, and Pamela Zave.  Ricky Butler and I also 
contributed. Our short piece was titled "Impediments to Industrial Use 
of Formal Methods." I was not particularly thrilled with the published 
article, because most of my rhetorically interesting sentences ended up 
being dulcified in the review process. But I fully supported the main 
points. Our article, and many of the others in the roundtable, could be 
republished today without modification, and be as accurate in 2017 as in 
1996.

More recently, but still a bit more than a decade ago, a well-known, 
highly-respected, very smart formal methods evangelist gave an invited 
talk at an FAA & NASA sponsored conference, before an audience of about 
200-250 engineers, engineering managers, and approval authorities. The 
condescending attitude of the speaker, his ignorance of the reality of 
commercial software development and assurance practices, his arrogant 
assertions of superior knowledge without any supporting evidence, and 
his thinly veiled claims of ethical failures in non formalists changed 
the attitudes of quite a few attendees. But not in the way he 
(presumably) hoped. Whereas many came to the conference thinking formal 
approaches may be able to help them, nearly all left the room after the 
talk thoroughly repulsed by the very idea. Someone may argue that the 
folks shouldn't have been so sensitive. That they should've been able to 
get past the bombastic rhetoric to the truth of the ideas presented. 
Perhaps. But arguing that way ignores human nature, and presupposes that 
evidence was presented about the truth of the ideas.

(Please note: The fact that this particular fellow in this particular 
talk didn't present any credible evidence to support his pro formal 
methods claims, does not mean, nor does it even imply, that no such 
evidence exists. Bad arguments for a claim should not convince anyone 
that the claim is true, but neither should they convince anyone that the 
claim is false, either.)

-- 
*C. Michael Holloway* (cMh)
[ Senior Research Computer Engineer | NASA Langley Research Center, 
Hampton VA USA | bit.ly/cmhpubs <http://bit.ly/cmhpubs> ]

Verba volant, scripta manent
spoken words fly away, written words remain

(The words in this message are mine alone; neither blame nor credit NASA 
for them.)


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171026/f3740645/attachment-0001.html>