Re: Rust's temporal safety for Ada/SPARK

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

"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:ofa4dh$15p$1@dont-email.me...
> On 05/14/2017 06:46 PM, digitalkevlar@gmail.com wrote:
>>
>> So, can someone today use Ada in a straight-forward way to write single- 
>> or
>> multi-threaded applications that are, in every use-case, totally immune 
>> at
>> compile-time to use-after-free and double-free errors with zero, runtime
>> overhead? Or can it not do that?
>
> Of course this is possible. It's very rare for well designed Ada to need 
> access types. An overwhelming majority of applications can be implemented 
> without ever writing "access".

I would suggest that Jeff's answer here should be read to say that 
"well-designed Ada code has no need for dynamic checks". Ada has plenty of 
unsafe constructs (for low-level memory managment, machine access, and the 
like), but one never has to use them. Ada after all is about combining 
safety with capability -- we try to allow everything (including unsafe 
stuff), but try to make it clear what is unsafe so that code review tools 
can determine what issues exist.

In any case, Ada code can be written so that there are no dereference checks 
and no dangling pointers. You obviously lose some capability when one does 
so. Does that matter? Depends on what you are doing.

Static rules (of any sort) are always going to reduce capability, 
*especially* when it comes to multithreaded programs. I find it highly 
unlikely that any sort of static rules would actually work in "every 
use-case". That's been claimed many times in the past, and it has always 
turned out that the claims were *way* overblown. The people making such 
claims often don't understand multithreading well enough. (It's an area, 
like random numbers and probability, that a little knowledge is more 
dangerous than no knowledge.)

I'm also very suspicious of any claims of new static rules simply because 
OOP pretty much forces dynamic checks if one uses references; strong typing 
breaks down for that and everything essentially becomes dynamic. There 
probably aren't any dereference checks, but you end up with dynamic type 
checks instead (substantially worse). Best thing is to avoid references 
altogether (but of course that too reduces capability).

                                  Randy.