Practitioners Reject Formal Methods Original
Please direct discussion to PractitionersRejectFormalMethodsDiscussion. This page is to present the context and reasoning in a clean and clear fashion, so people can see the point under discussion.
Reading some of EwDijkstra's papers again, a came across a paper entitled: On the Economy of doing Mathematics. In this paper EWD discussing constructing programs in a formal fashion from clear mathematical principles. I personally have various concerns about FormalMethods, but I have concerns about all "methodologies" and "bullets", silver or otherwise. I believe that they deserve a greater role than they currently have, and that they are dismissed all too quickly by those who don't really understand them.
However, this paper suggests various reasons for the apparent (then - this was 1992!) loss of faith in the mathematical construction of programs. I'm not convinced there ever was any faith in such an approach, but I was especially interested in one of EWD's percieved reasons. Hence this page.
I strongly urge you to read the original before launching into the usual collection of criticisms. A PDF of a scan of the hand-written original is here.
Remember, this is just one small part of a lengthy and carefully written paper. You may not agree with him, but I think there are truths here. Dismissing them out of hand runs the risk of missing something valuable.
The specific reason that drew my attention was this one:
- "FormalMethods are no good because the practitioner rejects them."
In response to this perceived objection to FormalMethods EWD writes:
- "This may sound convincing to you, but only if you don't know the practitioners. My eyes were opened more than 20 years ago on a lecturing trip to Paris with, on the way back, a performance in Brussels. It was the first time I showed to foreign audiences how to write programs that were intended to be correct by construction. In Paris, my talk was very well-received, half the audience getting about as excited as I was; in Brussels, however, the talk fell flat on its face: it was a complete flop. I was addressing the people at a large software house, and in my innocence I had expected them to be interested in a way of designing programs sich that one could keep them firmly under one's intellectual control. The management of the company, which derived its financial stability from its maintenance contracts, felt the design not to be in the company's interest, so they rejected my recommendations for sound commercial reasons. The programmers, to my surprise, rejected them too: for them, programming was tedious, but debugging was fun! It turned out that they derived the major part of their professional excitement from not quite understanding what they were doing and from chasing the bugs that should not have been introduced in the first place.
- "In short: formal techniques are rejected by those practitioners that are hackers instead of professionals."
Please direct discussion to PractitionersRejectFormalMethodsDiscussion.