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: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!news.stack.nl!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: Tue, 14 May 2013 14:02:32 -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> <1wzphazeho17m$.zy00zh7l7yu5$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1368558154 6164 69.95.181.76 (14 May 2013 19:02:34 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 14 May 2013 19:02:34 +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 Xref: news.eternal-september.org comp.lang.ada:15559 Date: 2013-05-14T14:02:32-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:1wzphazeho17m$.zy00zh7l7yu5$.dlg@40tude.net... > On Mon, 13 May 2013 22:01:56 -0500, Randy Brukardt wrote: ... >> 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. > > You are saying that there are political reasons not to do this. I am fully > aware of this. I am not a politician and have not idea how to deal with > that. My point is that these reasons are NOT technical ones. Two points here: (1) Virtually all constraints are political, not technical. Without the constraints posed by cost, compatibility, and the like, essentially anything is possible. Especially in software. One of the first problems we had to solve when starting as one of the Ada 9x User-Implementer teams was how to answer the question of implementability that we were supposed to provide feedback on. Virtually everything is implementable with enough effort (and levels of indirection); the question was where to draw the line. Eventually, we found that the question had been posed incorrectly; the Ada 9x team wanted to know about any implementation difficulties so they could sort out whether or not to change the feature to reduce the issues. Indeed, you could consider Ada's goals like readability and maintainability to be political, rather than technical, constraints. So pretty much anything that could be proposed is going to have to deal with the various political constraints -- they *cannot* be ignored in any real-world scenario. I'm not a politician either, and I'd rather avoid those sorts of games, but one has to do what it takes to get things done. > You suggest that there could be a way to convince people like you by > presenting some formalism? Seriously? You would reject the formalism using > same methods you and others did before. We could not even agree on the > notion of type! Not even on IMPROTANCE of types for Ada! You might be right. The only sure-fire way to convince everyone would be to write wording for the entire proposal and as well have a prototype implementation. If the prototype implementation were to show only minor incompatibilities when processing existing Ada code (including the ACATS, AdaCore test suite, and the like), that would be clear evidence that it is OK. But I'm quite aware that that's impractical. (Which is the crux of the problem, of course.) I suspect that you might be able to convince some people if you provided a fully fleshed out proposal with revisions to the wording of the Standard. That would mitigate the terminology problem because you would have to provide definitions for all of the terms that you use. But I suspect that it also too large a job for one person (as someone who has undertook smaller revisions that took a *long* time, like the revisions to support the aspect terminology -- and the language has long had some of that terminology, I wasn't quite starting from scratch.) When I was talking about a semi-formal proof above, I was thinking of it layered on top of fully fleshed out wording. I don't think you're every going to get much interest without that, precisely because of the issues with terminology. Randy.