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
Date: 1999-09-29T00:00:00+00:00 [thread overview]
Message-ID: <wccwvta6ius.fsf@world.std.com> (raw)
In-Reply-To: 7sr6gl$soc@dfw-ixnews19.ix.netcom.com
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.
next prev parent reply other threads:[~1999-09-29 0:00 UTC|newest]
Thread overview: 69+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-09-08 0:00 Array of Variant Records Question Bruce Detter
1999-09-08 0:00 ` Ted Dennison
1999-09-08 0:00 ` Matthew Heaney
1999-09-08 0:00 ` Mike Silva
1999-09-08 0:00 ` Matthew Heaney
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Matthew Heaney
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Matthew Heaney
1999-09-10 0:00 ` Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-11 0:00 ` Robert Dewar
1999-09-10 0:00 ` Robert Dewar
1999-09-10 0:00 ` Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-11 0:00 ` Jean-Pierre Rosen
1999-09-14 0:00 ` "cast away const" (was Re: Array of Variant Records Question...) Mark Lundquist
[not found] ` <wccd7viiv59.fsf@world.std.com>
1999-09-22 0:00 ` Array of Variant Records Question Robert I. Eachus
[not found] ` <7rrmqd$l89@drn.newsguy.com>
[not found] ` <wcciu59n2uf.fsf@world.std.com>
1999-09-22 0:00 ` Robert I. Eachus
1999-09-23 0:00 ` Robert Dewar
1999-09-23 0:00 ` Robert I. Eachus
1999-09-11 0:00 ` Richard D Riehle
1999-09-13 0:00 ` Hyman Rosen
1999-09-14 0:00 ` Mark Lundquist
[not found] ` <7roohh$s6r@dfw-ixnews7.ix.netcom.com>
[not found] ` <37e01168@news1.prserv.net>
[not found] ` <7rp86o$c6h@dfw-ixnews3.ix.netcom.com>
[not found] ` <37E18CC6.C8D431B@rational.com>
[not found] ` <7rs8bn$s6@dfw-ixnews4.ix.netcom.com>
[not found] ` <wccemfxn15s.fsf@world.std.com>
1999-09-22 0:00 ` 'constant functions' and access constant params (was Re: Array of Variant Records Question...) Richard D Riehle
[not found] ` <37e2e58c@news1.prserv.net>
1999-09-22 0:00 ` Richard D Riehle
1999-09-22 0:00 ` Matthew Heaney
1999-09-22 0:00 ` Richard D Riehle
1999-09-22 0:00 ` Matthew Heaney
1999-09-22 0:00 ` Matthew Heaney
1999-09-23 0:00 ` Vincent Marciante
1999-09-23 0:00 ` Matthew Heaney
1999-09-24 0:00 ` Robert A Duff
1999-09-25 0:00 ` Matthew Heaney
1999-09-27 0:00 ` Richard D Riehle
1999-09-27 0:00 ` Richard D Riehle
1999-09-27 0:00 ` David Kristola
1999-09-23 0:00 ` Robert Dewar
1999-09-27 0:00 ` Richard D Riehle
1999-09-28 0:00 ` Robert Dewar
1999-09-28 0:00 ` Richard D Riehle
1999-09-29 0:00 ` Robert Dewar
1999-09-29 0:00 ` Robert A Duff [this message]
1999-09-28 0:00 ` Robert Dewar
1999-09-28 0:00 ` "Competence" (was: 'constant functions' and access constant params) Ted Dennison
1999-09-28 0:00 ` Robert Dewar
1999-09-22 0:00 ` 'constant functions' and access constant params (was Re: Array of Variant Records Question...) Mark Lundquist
1999-09-22 0:00 ` Mark Lundquist
1999-09-09 0:00 ` Array of Variant Records Question Brian Rogoff
1999-09-13 0:00 ` Matthew Heaney
1999-09-13 0:00 ` Robert A Duff
1999-09-13 0:00 ` Matthew Heaney
1999-09-13 0:00 ` Brian Rogoff
1999-09-14 0:00 ` Robert Dewar
1999-09-14 0:00 ` Brian Rogoff
1999-09-14 0:00 ` Robert Dewar
1999-09-10 0:00 ` Proposed Ada features (was Re: Array of Variant Records Question...) Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-10 0:00 ` tmoran
1999-09-09 0:00 ` Array of Variant Records Question Matthew Heaney
1999-09-09 0:00 ` Mark Lundquist
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Nick Roberts
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Tucker Taft
1999-09-10 0:00 ` Nick Roberts
1999-09-08 0:00 ` Thank you Bruce Detter
1999-09-08 0:00 ` Martin C. Carlisle
1999-09-08 0:00 ` Array of Variant Records Question Martin C. Carlisle
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox