Re: A hole in Ada type safety

["Randy Brukardt" <randy@rrsoftware.com>]

"Florian Weimer" <fw@deneb.enyo.de> wrote in message 
news:87tydfbtp3.fsf@mid.deneb.enyo.de...
...
> And once there is something like this in the language, it is difficult
> to decide if a new addition (such as aliased parameters) make things
> worse or not.

Not sure how something that adds new capabilities only for elementary types 
could make anything worse.

We also ran across this particular erroneousness in another case; we decided 
that we had to let subprograms trust their constraints (which introduces 
some additional erroneousness) as the alternative requires a lot of 
additional code for discriminanted parameters. (I forget where the wording 
change for that ended up.)

Cases like this is why I like to say that all real Ada programs are 
erroneous, so any result is allowed. :-) If you could write an entire 
program in SPARK, that could make that statement a falsehood, but the Ada 
runtime is most likely erroneous for some reason (interfacing to C tends to 
end up erroneous in some cases, for instance). You'd probably need a SPARK 
runtime on top of a SPARK OS in order to make a non-erroneous program a 
reality.

                              Randy.