Re: Rust's temporal safety for Ada/SPARK

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2017-05-14 18:46, digitalkevlar@gmail.com wrote:

> Niklas Holsti's post shows he understands what capability I'm 
> describing. Rust code can be shown free of double-free's and 
> dangling-pointers at *compile-time* with *no runtime checks or GC*.
> It does it with just a few simple rules. Here's the simplest,
> shortest description I could find to save you all time: >
 > 
https://stackoverflow.com/questions/36136201/how-does-rust-guarantee-memory-safety-and-prevent-segfaults

Helpful would be to have an example where pointers are needed. The 
example provided requires no pointers. So in Ada case, no such problem 
exist at all.

[...]

> 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?
Without having other examples, the answer is: there is no such problem 
in Ada because arguments of task rendezvous are not pointers.

For multitasking, problems arise when the method of problem 
decomposition requires constructs which are not safe in the sense that 
safety is statically undecidable. Which means that a decidable static 
constraints would simply kill the algorithm.

 From the practical perspective it is usually possible to trade one 
danger for another (lesser, greater, equal), e.g. to exchange deadlock 
for livelock, but not getting rid of it altogether.

Considering the problem of having tasking safe per construction, my 
impression is that constraints are no or very little help. Additional 
methods of decomposition are.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de