djones@megatest.UUCP (Dave Jones) (03/01/90)
I finally got around to reading the debate on teaching 'Computing
Science' in December's _Communications of the ACM_.
As I began, I was keen to hear Edgar let 'em have it. Being an
aspiring curmudgeon myself, I am always eager to witness a real master
whipping through the ranks of intelligentsia, exposing the pompous as
trivial, and deflating egos like so many corn souffles. I'd heard that
Dijkstra is the best -- a past master of curmudgery. Besides, I had worked
through his _Discipline_of_Programming_ and even used it for lecture notes
when I was a visiting associate professor. I thought it was a darn good
text. Beat the hell out of _Oh! Pascal_, that's for sure.
And "Oh goody!" I thought. His principle rival is this Parnas guy. I'm still
mad at him for wasting about six hours of my time when, years ago, I tediously
dug through the clumsy notation and imprecise language in a Communications
article, only to discover that the 'it-ti' construct was no big deal, and
that his 'proof' that it was stronger than Dijkstra's 'do-od' was full of, uh,
holes. Indeed, I easily proved that 'it-ti' had exactly the same strength.
(I was tempted to invent my own construct called 'do-od-it-ti' and name the
programming language 'Redbone'.) It would be good, after all these years,
to witness Dijkstra taking him apart.
So in I dug. It took Dr. D. quite a few paragraphs to get around to
the meat of the subject, but along the way he managed to get in a couple of
zingers. I particularly enjoyed, 'software engineering has accepted as its
charter, "How to program if you cannot."' Yeah, get 'em Edgar. Go for it!
Then came shock number 1.
About half way through the article it struck me quite suddenly:
This guy does not have a clue! At one point he says, "The programmer's
task is ... to give a formal proof that the program he proposes meets
the equally formal functional specification." Is that really what he
thinks a programmer's job is? A human formal language translator? I've been
in this business off and on for nineteen years -- full time the past eleven --
and I have yet to be asked to do a formal proof of correctness! From time
to time I may undertake to prove something using formal methods, but only
as a means to an end. My job is to build a product or, more often, to
modify an existing one, to make it dependable, and to deliver it on time.
Often I must collaborate with the marketing department or with customers in
order to specify better what the product is to be. Disjktra's 'equally formal
functional specification', if it exists at all, is likely to be as much the
doing of the programmer as of anyone else. I was reminded of Brad Cox, who
has argued that formal specifications tend to be used principally for
defence against change.
Next was shock number 2.
Parnas made good sense. He effectively exposed several of Dijkstra's strange
delusions, and put things in pretty good perspective. I was losing heros and
villains left and right.
Several other people had a go at it. The very best reply, in my opinion, was
by Terry Winograd of Stanford. He began,
Behind Disjktra's bravado and invective there lurks a coherent
argument about the nature of computer science education. Coherent
and interesting, but wrong, because it is based on faulty premises.
To start out with Disjktra is wrong about what computers do, wrong
about what programmers do, and wrong about what engineers do.
He went on to prove his points one by one, (albeit, not to any formal
specification).
Disjktra's counter-rebuttal was subdued. He said that he had only been
proposing an introductory programming course for freshman, after all, and
admitted that the 'choice of functional specifications' was not all that easy.
Back in the piney woods we used to call this kind of thing 'crawfishing',
after that crustacean's habit of creeping backwards as he flexed his pincers.
As to people's doubts about the effectiveness of formal proof methods,
Dijkstra said that he had once shared such doubts, but over the course of
the last decade, they had 'evaporated'. Good choice of words there, Edgar.
Next time, put a lid on it.