Re:Why you should, actually, rewrite some of it in Rust
by dikaiosune on Wednesday July 12, 2017 @01:05PM
(#14754271)
Please correct me if I'm wrong, but don't Ada/SPARK's memory safety guarantees only hold when all memory is pre-allocated? My memory is that dynamic allocations aren't visible to the proof system (this may be in plain Ada without SPARK, now that I think of it).
[ Parent
| on HN ]
Re:Why you should, actually, rewrite some of it in Rust
by pcwalton on Wednesday July 12, 2017 @02:34PM
(#14755222)
That is correct. Ada and SPARK do not provide memory safety in the case of dynamic memory allocation without garbage collection.
Re:Why you should, actually, rewrite some of it in Rust
by touisteur on Wednesday July 12, 2017 @04:41PM
(#14756465)
Not as much as rust, but still. I'm not sure whether it qualifies as memory safety for you but using Controlled types alleviates a large part of the problems of dynamic memory allocation. http://www.adacore.com/knowledge/technical-papers/the-gnat-i... might be of interest for the underlying implementation.
I also find that 'not null' access types, typed pointers and in general the in/out/in-out parameter passing mode help making ownership clearer... And there's also the limited types in the toolbox, to 'hide' ugly pointers/resource ids, etc.
Spark2014 still excludes pointers and aliasing, but I think some work is in progress. Previous HN thread : https://news.ycombinator.com/item?id=14346032