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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Safety of unprotected concurrent operations on constant objects
Date: Thu, 15 May 2014 16:27:30 +0200
Organization: cbb software GmbH
Message-ID: <oiqjtov5sngt$.2785yqcvqig5$.dlg@40tude.net>
References: <slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu>
 <lyzjiw7h6c.fsf@pushface.org> <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>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: QTaafVZuunHujkJPndFR7g.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:19846
Date: 2014-05-15T16:27:30+02:00
List-Id: <comp.lang.ada>

On Thu, 15 May 2014 09:21:14 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> You *cannot* increase the power of prover later on, as you and others seem
>> to suggest.
> 
> Why not?

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

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

Example from existing Ada:

   function Foo return Integer is
   begin
      raise Constraint_Error;
   end Foo;

This program is illegal, though GNAT posses the power to prove Foo's
"contract" fulfilled (vaguely: no junk result returned). Yet the language
requires this power constrained. The mandated power is that it is
non-provable that the code following raise were unreachable.

--------------
* If we talk about contracts proper. Per definition, a contract violation
makes the program illegal

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de