[SystemSafety] Bursting the anti formal methods bubble
C. Michael Holloway
c.m.holloway at nasa.gov
Thu Oct 26 15:09:40 CEST 2017
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>
More information about the systemsafety
mailing list