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,39579ad87542da0e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.38.5 with SMTP id c5mr1645010wik.3.1368583610693;
        Tue, 14 May 2013 19:06:50 -0700 (PDT)
Path: 
 hg5ni110155wib.1!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.stack.nl!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
Date: Fri, 10 May 2013 09:49:35 +0200
Organization: cbb software GmbH
Message-ID: <1jc46ynzptlxm.1fafjhr8hlblq.dlg@40tude.net>
References: <op.wv8jh1c1ule2fv@cardamome> <op.wwbvqzkeule2fv@cardamome>
 <op.wwnp2zkrule2fv@cardamome> <u3jaslg5kca7.1gk5ds3d4sx2y$.dlg@40tude.net>
 <op.wwnsmtteule2fv@cardamome> <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net>
 <op.wwny5jerule2fv@cardamome> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net>
 <op.wwn4oak8ule2fv@cardamome> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net>
 <kmbohm$elb$1@loke.gir.dk> <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net>
 <kmebjm$eds$1@loke.gir.dk> <1bp6zlpetr5l4.12a9zcd1x3yya.dlg@40tude.net>
 <kmh5a3$sfb$1@loke.gir.dk>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: 15waz9CoS+eMakbyhTPyFQ.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: 2013-05-10T09:49:35+02:00
List-Id: <comp.lang.ada>

On Thu, 9 May 2013 16:43:29 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1bp6zlpetr5l4.12a9zcd1x3yya.dlg@40tude.net...

>> Because most of Ada semantics is OK. I don't see any mistakes. Even if they
>> were, it is irrelevant because I am looking for a more general model, where
>> mistake or not, it becomes just an implementation. So if you don't like a
>> particular built-in type for whatever reason, you make your own. No
>> problem.
> 
> When you say "semantics", you're really only talking about the dynamic 
> semantics, that is the runtime model. But the compile-time model is just as 
> important. You would have to reproduce every feature and flaw of the 
> existing compile-time model with a totally new underlying model. And doing 
> that would be very, very complex.

Exactly.

> The problem is, when you do that, you'd have no way to determine whether or 
> not it is really compatible. (After all, there is no formal model for Ada, 
> and there never has been.) Ada's definition is just a mass of English text, 
> and replacing it by a different mass of English text leaves one no practical 
> way to prove compatibility.

Why should I need it if no existing Ada compiler does that? It will be as
compatible as any existing Ada implementation is. There is no reason to
require more than that, e.g. formal verification.

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