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: Martin Dowie <martin@dowie-cs.demon.co.uk>
Subject: Re: No Go To's Forever!
Date: 2000/03/29
Message-ID: <38E1F6D5.8303903C@dowie-cs.demon.co.uk>#1/1
X-Deja-AN: 603829549
Content-Transfer-Encoding: 7bit
X-NNTP-Posting-Host: dowie-cs.demon.co.uk:193.237.34.207
References: <8bbsc6$aes$1@nnrp1.deja.com>
 <HRkC4.1999$U95.38761@news.pacbell.net> <8bdbof$t19$1@nnrp1.deja.com>
X-Accept-Language: en
Content-Type: text/plain; charset=us-ascii
X-Complaints-To: abuse@demon.net
X-Trace: news.demon.co.uk 954332899 nnrp-07:5786 NO-IDENT
 dowie-cs.demon.co.uk:193.237.34.207
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Date: 2000-03-29T00:00:00+00:00
List-Id: <comp.lang.ada>

speaking of proving things...

one of the reasons I had always been told for avoiding using gotos, was
that it makes a program unprovable. a) was this true; and if so, b) is
this still true?

Robert Dewar wrote:

> Of course it is different, it does a different sequence of
> computations. The algorithm you give is computationally
> equivalent, but you actually need to prove this, it is not
> self evident! An algorithm is a prescription for a sequence
> of computations, a different sequence is a different algorithm!