ian@oravax.UUCP (Ian Sutherland) (02/11/90)
In article <20116@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes: >In article <1291@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes: >me>>[Turing's] `proofs' in no way differ from >me>>what software engineers would call `design documentation.' >> >>This claim is truly hard to let pass. I have read plenty of "design >In view of this message I looked over some program documentation >and texts I snarfed >from some folks I once worked with. It struck me that their >documentation was quite similar to mathematical proofs -- if anything >more detailed because they didn't assume the reader was as literate >as a math journal editor might. They also included careful references >to results in the literature. > >Why the discrepency between Mr. Sutherlands experiences and my own? >I asked myself. Then it struck me -- perhaps Mr. Sutherland had been >working with CS majors, who often cannot organize their thoughts or even >design a program before it's finished. Am I right? No, you are not. In fact, you are not even close. Is there any of this documentation which resembles mathematics that you can send me Mr. Watters? I'd truly like to see it. If what you say is true, it must be vastly different than most documentation of ANY kind that I've ever seen. Oh, and just to be fair, if you want to see the kind of crummy documentation that I claim I've seen, I'll be glad to send you some, or you can just look at the manuals for almost any commonly used OS. >My colleagues >had no formal training in CS -- they were physicists, mathematicians >and electrical engineers by training. For each of the disciplines you've mentioned (including CS), I've met people who did good documentation and people who did bad. I don't think it has much to do with which of these areas you come from, and I think your nasty cracks are inappropriate. >Anyway, why would making everything formal solve this? It seems to >me that the same CS majors would write equal gibberish as a `formal >specification' and prove that their gibberish programs are therefore >formally correct. You are misremembering the course of this discussion Mr. Watters. The argument I have been making is that doing formal proofs that a program meets a specification gives you greater assurance that the program meets the specification. I have not claimed that doing formal specification makes it more likely that you will write the correct specification. In fact, with the current state of formal specification languages, unless the specification writer knows how to use the specification language carefully, he will be MORE likely to write an incorrect specification than if he wrote down a detailed description in "mathematical English" of what the program is supposed to do. I will just note in passing that a good portion of the specifications I've read have been so vague that it was not even clear what it would MEAN for the program to satisfy them. -- Ian Sutherland ian%oravax.uucp@cu-arpa.cs.cornell.edu Sans Peur