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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.157.28.157 with SMTP id l29mr285789ota.60.1494977871474; Tue, 16 May 2017 16:37:51 -0700 (PDT) X-Received: by 10.157.82.15 with SMTP id e15mr10700oth.6.1494977871445; Tue, 16 May 2017 16:37:51 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!67no32600itx.0!news-out.google.com!m134ni152itb.0!nntp.google.com!67no32397itx.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 16 May 2017 16:37:51 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.113.92.25; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 76.113.92.25 References: <1c0e2c7c-4fd6-43d1-9848-f03e1a72bcb3@googlegroups.com> <40fc8c30-08d6-4456-a488-a1b28615953b@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <33bea28a-f571-42bc-a2c6-0e01c02b0744@googlegroups.com> Subject: Re: Rust's temporal safety for Ada/SPARK From: Shark8 Injection-Date: Tue, 16 May 2017 23:37:51 +0000 Content-Type: text/plain; charset="UTF-8" Xref: news.eternal-september.org comp.lang.ada:46802 Date: 2017-05-16T16:37:51-07:00 List-Id: On Tuesday, May 16, 2017 at 3:36:55 PM UTC-6, Randy Brukardt wrote: > My concern is that one almost always has to use access-to-classwide types in > an Ada context as it is impossible to do "co-derivation" so that a type and > its static reference type get derived together. One can use dispatching to > cover some of the pain, but that of course is dynamic itself and can cause > other issues. (And the problem is even worse if one uses an abstract handle > as the containers do, as dispatching no longer is an option.) Which is why we have access parameters in read/write/input/output as well as the generic-dispatching constructor, right? -- That's one of the biggest pain-points I'm having with SPARK: I want to be able to use stream-attributes AND have verification! While the mode-specification in Ada is pretty great (describing data-flow rather than mechanics) it does lead to a pretty painful problem w/ classwide parameters: combined with how you constrained values/type-passing works you can't have a Procedure Visitor( Item : in out Node'Class ) is -- On some condition replace Item with value of Make_More_Specific_Node( Item ) and instead have to have a Procedure Visitor( Item : in out access Node'Class ) is -- On some condition replace Item.all with value of Make_More_Specific_Node( Item ) It's really quite irritating (and IMO disappointing) that "access" was added as a mode-indicator/-modifier.