using break <label> ... and program proofs

[Dick Dunn]

> 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.