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=unavailable autolearn_force=no version=3.4.4 Path: border1.nntp.ams3.giganews.com!border1.nntp.ams2.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!news.mixmin.net!newsfeed.fsmpi.rwth-aachen.de!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Mon, 13 May 2013 22:01:56 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <1bp6zlpetr5l4.12a9zcd1x3yya.dlg@40tude.net> <1jc46ynzptlxm.1fafjhr8hlblq.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1368500516 11356 69.95.181.76 (14 May 2013 03:01:56 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 14 May 2013 03:01:56 +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-Original-Bytes: 4582 Xref: number.nntp.dca.giganews.com comp.lang.ada:181627 Date: 2013-05-13T22:01:56-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:bkozr3g5i0hk$.15qnfap6hrj20$.dlg@40tude.net... > On Fri, 10 May 2013 19:09:12 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" 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. > > You didn't answer the question. If it goes without a proof now, why can it > continue so? I'm afraid I don't understand your question, so I can't answer it directly. I can only repeat the situation: You are proposing a complete overhaul of the model of types in Ada. You keep claiming that this overhaul would be compatible without a shred of proof that this is achievable. You would have to find *some* way to convince the Ada community that your revised model is in fact 100% compatible with the current model. A semi-formal proof would clearly be the best way to do that. Remember that Ada is defined in English, and as such there is not currently a formal way to tell if we're staying compatible. As such, there is a great reluctance to make major changes to the text, because there is no way to find regression errors. Our experience has been that we introduce about as many serious bugs to the standard as we make changes to it, simply because we can't easily tell when we break things. As such, there would have to be an amazingly serious problem that absolutely had to be fixed in Ada for us to consider any major change to the model -- even if such a model would be an improvement. The only sure-fire way to get a level of confidence in such a model would be to provide extrodinary proof of its correctness compared to the existing standard. And that's all I'm talking about when I say a "semi-formal proof" is needed. Randy.