Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/17/84; site opus.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!allegra!mit-eddie!godot!harvard!seismo!hao!cires!nbires!opus!rcd
From: rcd@opus.UUCP (Dick Dunn)
Newsgroups: net.lang.c
Subject: Re: using break <label> ... and program proofs
Message-ID: <1027@opus.UUCP>
Date: Thu, 17-Jan-85 01:11:58 EST
Article-I.D.: opus.1027
Posted: Thu Jan 17 01:11:58 1985
Date-Received: Sat, 19-Jan-85 01:40:00 EST
References: <7283@brl-tgr.ARPA>
Organization: NBI,Inc, Boulder CO
Lines: 21

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