3 ms·

How about Ada/SPARK then?

• dikaiosune 9y ago
  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).
  • pcwalton 9y ago
    That is correct. Ada and SPARK do not provide memory safety in the case of dynamic memory allocation without garbage collection.
    • touisteur 9y ago
      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-implementation-of-controlled-types/ 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 https://news.ycombinator.com/item?id=14346032