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
X-Google-Thread: a07f3367d7,aba1514f4a1fc450
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.181.11.234 with SMTP id el10mr1247736wid.2.1345989645106;
        Sun, 26 Aug 2012 07:00:45 -0700 (PDT)
Path: 
 e9ni24215856wia.0!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.84.MISMATCH!newsfeed.xs4all.nl!newsfeed5.news.xs4all.nl!xs4all!newspeer1.nac.net!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!news.snarked.org!newsfeed.news.ucla.edu!ihnp4.UCSD.Edu!nntp.ucr.edu!solaris.cc.vt.edu!news.vt.edu!news.glorb.com!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.arch,comp.lang.ada
Subject: Re: Have the Itanium critics all been proven wrong?
Date: Wed, 22 Aug 2012 12:14:11 +0200
Organization: cbb software GmbH
Message-ID: <1sllfduhqrk66$.1fevpf4v7e4di$.dlg@40tude.net>
References: <5021874F.1747D0BF@sonic.net> <1e1tf9-0kp2.ln1@ntp6.tmsw.no>
 <k0gn5r$l9h$1@needham.csi.cam.ac.uk> <GPRWr.31944$Bw1.31300@newsfe05.iad>
 <k0gq97$li8$1@needham.csi.cam.ac.uk> <k0h6ef$jke$1@speranza.aioe.org>
 <46f19bfc-930e-4f06-b5a6-c60f39cfda0c@p14g2000yqk.googlegroups.com>
 <k0r609$4ij$1@speranza.aioe.org>
 <077b12f6-1196-4b5c-bbdb-04291b1ae616@q22g2000vbx.googlegroups.com>
 <k0rree$lkn$1@speranza.aioe.org> <CC5730C5.1BC2E%yaldnif.w@blueyonder.co.uk>
 <k0t67b$b8r$1@speranza.aioe.org> <CC585119.1BCCC%yaldnif.w@blueyonder.co.uk>
 <k0uenp$fbg$1@speranza.aioe.org> <k0vo9u$fer$1@dont-email.me>
 <589825d2-d998-456a-9c37-c8ae13e1e7bc@e29g2000vbm.googlegroups.com>
 <a9iagtF1rqU1@mid.individual.net>
 <4c83f0f4-30e2-44bd-8b73-ada05de9322b@q22g2000vbx.googlegroups.com>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-08-22T12:14:11+02:00
List-Id: <comp.lang.ada>

On Wed, 22 Aug 2012 02:29:21 -0700 (PDT), Michael S wrote:

> So let's do not call it "two languages". Let's talk about "full Ada"
> and "checked Ada" where "checked Ada" is a subset in which "it is not
> possible to clobber arbitrary memory locations". Hopefully  "checked
> Ada" is still much closer in # features to the "full Ada" than to
> SPARK.

I don't understand why people keep on talking about two languages.
Annotations should be optional like Unchecked_Deallocation is. If you
annotate some Ada program unit, you might prove certain things about that
unit. An conversely if you upfront require certain propositions to be
proved/provable about given units you have to annotate something in these.
Why two languages?

The only real problem is the power of the prover to mandate.

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