From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,14f7200925acb579
X-Google-Attributes: gid103376,public
From: Robert A Duff <bobduff@world.std.com>
Subject: Re: No Go To's Forever!
Date: 2000/04/01
Message-ID: <wcc7lehg5yd.fsf@world.std.com>#1/1
X-Deja-AN: 605295035
Sender: bobduff@world.std.com (Robert A Duff)
References: <8bbsc6$aes$1@nnrp1.deja.com>
 <HRkC4.1999$U95.38761@news.pacbell.net> <8bdbof$t19$1@nnrp1.deja.com>
 <38E1F6D5.8303903C@dowie-cs.demon.co.uk>
 <874s9p7jwi.fsf@deneb.cygnus.argh.org> <8bu48a$3tt$1@nnrp1.deja.com>
 <wcczorgbgwi.fsf@world.std.com> <8c50hn$hvb$1@nnrp1.deja.com>
Organization: The World Public Access UNIX, Brookline, MA
Newsgroups: comp.lang.ada
Date: 2000-04-01T00:00:00+00:00
List-Id: <comp.lang.ada>

Robert Dewar <robert_dewar@my-deja.com> writes:

> In article <wcczorgbgwi.fsf@world.std.com>,
>   Robert A Duff <bobduff@world.std.com> wrote:
> > Robert Dewar <robert_dewar@my-deja.com> writes:
> >
> > > On the other hand, you can prove certain properties of a
> program
> > > without a spec, e.g. that it terminates for all inputs, or
> that
> > > it cannot raise an exception etc.
> >
> > To me, that seems like a more useful approach in most
> > circumstances.
> 
> I would have said more practical.

Agreed.

And we should never forget that there are some things that can't be
proven because they can't be formalized, but are still important
requirements.  Eg informative error messages from a compiler.

- Bob