rcd@opus.UUCP (Dick Dunn) (01/17/85)
> Whoa! I'm not out to automate current design practices. I'm much > more interested in providing a NEW design methodology whereby the > compiler (or some other entity - like lint for C) goes through and > either (1) proves your program correct or (2) derives a provably > correct program from a proof of an algorimth. > > Work is currently being done on both these topics on a very small > scale, and things look quite promising except for the fact that doing > these things take mega-cycles... I'm not impressed by any argument based on program proof, for the simple reason that the essence of the above statement--"we want to prove programs, we think we can do it and we've done something with small programs; all we have to do is scale it"--has been true for AT LEAST ten years. A brief, lucid discussion of the scaling problem can be found in "Notes on Structured Programming", Dijkstra, in the book _Structured_Programming_ by Dahl, Dijkstra, and Hoare. -- Dick Dunn {hao,ucbvax,allegra}!nbires!rcd (303)444-5710 x3086 ...A friend of the devil is a friend of mine.