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: 
 border1.nntp.dca3.giganews.com!backlog3.nntp.dca3.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!zen.net.uk!dedekind.zen.co.uk!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 10:03:20 +0200
Organization: cbb software GmbH
Message-ID: <8w0te2yerch4$.1ll2fpovfkuzx.dlg@40tude.net>
References: <slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu>
 <scy9v.1071029$2N5.142769@fx05.iad> <kxy9v.109149$f85.89664@fx19.iad>
 <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>
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
X-Original-Bytes: 2924
Xref: number.nntp.dca.giganews.com comp.lang.ada:186422
Date: 2014-05-15T10:03:20+02:00
List-Id: <comp.lang.ada>

On Tue, 13 May 2014 15:27:02 -0500, Randy Brukardt wrote:

> (Besides, I think 
> that mandating proof would have the effect of driving all Ada vendors other 
> than AdaCore out of the Ada business -- I very much doubt that any of the 
> other compiler vendors could afford the investment. Perhaps that will happen 
> anyway, given the slow uptake of Ada 2012 by other vendors.)

No, that is not the idea. Ada would not mandate any proofs. The programmer
will.

Task safety or whatever, will be a library of axioms and inference rules.
The language should provide means of encapsulation and reuse for
annotations.

If you don't want to annotate the contracts of your package with these, you
don't. With *proper* contracts that must have no effect on the program
semantics. Regarding legality, removing a contract cannot make a program
illegal (preconditions weakened, postconditions strengthened).

The only tricky thing the standard should define is the power of the prover
and its *weakness*. because in order to be portable the prover must reject
provable cases which other provers might not be able to prove.

You *cannot* increase the power of prover later on, as you and others seem
to suggest.

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