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.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!us.feeder.erje.net!nntp.club.cc.cmu.edu!micro-heart-of-gold.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!.POSTED!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: Safety of unprotected concurrent operations on constant objects
Date: Thu, 15 May 2014 11:53:09 -0400
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wccsiobqbru.fsf@shell01.TheWorld.com>
References: <slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu>
 <fRN9v.204655$Ng5.180587@fx17.iad>
 <t7a0jcl05g1h.11jb75b2jg1l7.dlg@40tude.net> <eT_9v.574$dr.264@fx27.iad>
 <83ha6vuynrzs.1jk08faxb8mnl.dlg@40tude.net> <xtDav.68151$7X2.15124@fx19.iad>
 <1jebi7cf92ak4.1trmstj8qi3wm.dlg@40tude.net> <zv4bv.5236$pa5.5140@fx23.iad>
 <1i6pyg077xlrv.vnwotzzgb0ut$.dlg@40tude.net> <nYobv.8538$116.7932@fx21.iad>
 <10pk27v48vhcb$.1qkf6roq2yzjn$.dlg@40tude.net> <RVObv.4489$TT7.3088@fx02.iad>
 <1qq0ryc8c4l2m.1driqwwiwwl02.dlg@40tude.net>
 <%vhcv.255737$s87.168969@fx11.iad>
 <fw1hrdv0jufx$.fetdmr8mer8o$.dlg@40tude.net> <qtqcv.27961$hv6.6727@fx17.iad>
 <1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net> <lktv6n$kit$1@loke.gir.dk>
 <8w0te2yerch4$.1ll2fpovfkuzx.dlg@40tude.net>
 <wcck39n6uut.fsf@shell01.TheWorld.com>
 <oiqjtov5sngt$.2785yqcvqig5$.dlg@40tude.net>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: pcls7.std.com 1400169187 17255 192.74.137.71 (15 May 2014 15:53:07
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Thu, 15 May 2014 15:53:07 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:64xmYz1ZTDLW2gZX85DtKWr7DIM=
Xref: news.eternal-september.org comp.lang.ada:19848
Date: 2014-05-15T11:53:09-04:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> Because inability to prove that contract X is fulfilled by a party P makes
> P illegal. [*]

I know that's your point of view.  I haven't seen you explain why.

Yeah, I know compile-time checks are good when possible.
But they're not always possible (as I'm sure you know).
So insisting on contracts being checked at compile time
doesn't make my programs better -- it just requires me to
put "--" before some of my contracts.

> Unless you accept making illegal programs legal, you must not allow the
> prover's power to change.

Every new version of Ada has made some previously-illegal programs
legal.  An infinite number of them, in fact.  So of course I 
accept making illegal programs legal.

- Bob