Re: Rust's temporal safety for Ada/SPARK

[Shark8 <onewingedshark@gmail.com>]

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.