Re: Rust's temporal safety for Ada/SPARK

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 17-05-14 20:36 , Jeffrey R. Carter wrote:
> 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.

Yes... if one does not have to meet stringent resource constraints 
(time, space) on limited HW.

> It's very rare for well designed Ada to need access types.

"Well designed" is of course subjective. The container library has made 
it practical to avoid access types in the application code, but then 
there are other potential run-time problems, such as "tampering" with 
the containers, which require run-time checks (and which are to some 
extent consequences of the use of access types within the container 
library).

> An overwhelming majority of applications can be
> implemented without ever writing "access".

I find it difficult to agree with that "overwhelming", at least if one 
includes the access types used under the covers in the container library.

Even in applications where heap allocation is forbidden, there are 
usually some dynamically allocated resources -- elements of "resource 
pools" such as message buffers -- with the corresponding 
application-defined "reference" data types, and the same problems of 
managing allocations over time. I don't know if Rust's memory-management 
scheme extends to such non-heap "references, however.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .