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,bd40601768eaf8fd
X-Google-Attributes: gid103376,public
From: Robert A Duff <bobduff@world.std.com>
Subject: Re: 'constant functions' and access constant params (was Re: Array of
 Variant Records Question...)
Date: 1999/09/29
Message-ID: <wccwvta6ius.fsf@world.std.com>#1/1
X-Deja-AN: 530677067
Sender: bobduff@world.std.com (Robert A Duff)
References: <7r5vh3$imu1@svlss.lmms.lmco.com> <37d6a45c@news1.prserv.net>
 <eExB3.6$ZR.1146@news.wenet.net> <37d6ccb6@news1.prserv.net>
 <7r77i8$i08$1@nnrp1.deja.com> <37d7c116@news1.prserv.net>
 <7r8t21$ov5$1@nnrp1.deja.com> <37d822a1@news1.prserv.net>
 <7reg02$t83@dfw-ixnews6.ix.netcom.com> <37DE8D09.C863CBC9@rational.com>
 <7roohh$s6r@dfw-ixnews7.ix.netcom.com> <37e01168@news1.prserv.net>
 <7rp86o$c6h@dfw-ixnews3.ix.netcom.com> <37E18CC6.C8D431B@rational.com>
 <7rs8bn$s6@dfw-ixnews4.ix.netcom.com> <37e2e58c@news1.prserv.net>
 <7s9nd0$cbe@dfw-ixnews17.ix.netcom.com> <37e8e067@news1.prserv.net>
 <7sas3p$bfa@dfw-ixnews3.ix.netcom.com> <7sc6b6$c6m$1@nnrp1.deja.com>
 <7socka$6u4@dfw-ixnews19.ix.netcom.com> <7sqbt6$1la$1@nnrp1.deja.com>
 <7sr6gl$soc@dfw-ixnews19.ix.netcom.com>
Organization: The World Public Access UNIX, Brookline, MA
Newsgroups: comp.lang.ada
Date: 1999-09-29T00:00:00+00:00
List-Id: <comp.lang.ada>

Richard D Riehle <laoXhai@ix.netcom.com> writes:

> I agree with most of your observations here.  Even Bertrand Meyer,
> advocate of "design by contract" through assertions, agrees that
> we have not yet reached a point in software design where we can
> rely on a compiler to "prove" the validity of an assertion. ...

It's not just that we haven't "yet" reached such a point.  Look at one
of Robert Dewar's favorite examples (also one of my favorites): An
important requirement for a compiler is to produce clear error messages.
But you can't *prove* anything like that (in the mathematical sense).
It's hard to see how anybody could *ever* prove it, because it seems
impossible to formalize the notion of a "clear error message" in a way
that doesn't lose the essense of that notion.

I think I remember an argument crossposted to here and comp.lang.eiffel,
in which both Robert and Bertrand Meyer participated.  As I recall,
Meyer's response to the above point was to deny that "clear error
messages" makes any sense as a requirement.  I claim it *does* make
sense.  Certainly, I know a bad error message when I see one.  You could
even *measure* it scientifically -- observe people programming, and
measure how long it takes them (on average) to figure out and fix what
the compiler is complaining about.  The fact that you can't prove
anything about it mathematically doesn't mean it's somehow unreal or
irrelevant.

I'm not sure I fully understood Meyer -- after all, Eiffel allows
*comments* as assertions, syntactically, which suggests that he allows
for the possibility of requirements that are not formalizable.

>...  Of
> greater concern is that one can construct an assertion so complex
> that no current theorem-proving software can guarantee its
> correctness.

I'm not sure how this differs from your previous point.

- Bob
-- 
Change robert to bob to get my real email address.  Sorry.