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=ham
	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.66.241.69 with SMTP id wg5mr4964307pac.2.1368583727948;
        Tue, 14 May 2013 19:08:47 -0700 (PDT)
MIME-Version: 1.0
Path: 
 bp1ni2274pbd.1!nntp.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!border4.nntp.dca.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.etla.org!feeder.erje.net!eu.feeder.erje.net!nuzba.szn.dk!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
Date: Fri, 10 May 2013 19:09:12 -0500
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <kmk278$t5m$1@loke.gir.dk>
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> <1jc46ynzptlxm.1fafjhr8hlblq.dlg@40tude.net>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: loke.gir.dk 1368230953 29878 69.95.181.76 (11 May 2013 00:09:13 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Sat, 11 May 2013 00:09:13 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-Received-Bytes: 2953
Date: 2013-05-10T19:09:12-05:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@40tude.net...
> On Thu, 9 May 2013 16:43:29 -0500, Randy Brukardt wrote:
...
>> 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.

Because there is no other way to tell. No one is going to implement it (or 
put it into the Standard) unless they know that it is "at least as 
compatible as an existing Ada implementation". You're going to have to prove 
that somehow, and that proof is going to have to be at least semi-formal, 
because it is going to have to be convincing. Handwaving in a forum like 
this is not a convincing proof.

                                    Randy.