[touisteur]

Hey thanks for the pointer to this thread. Allowing pointers in SPARK would be incredible... Today SPARK is so interesting because it's not all-or-nothing. So some parts can be SPARK (with different levels of proof), others Ada, etc.

One of the main limitations of the tech is 'no pointers' in SPARK mode. There are some tricks to hide pointers (you may want to look up the SPARK deployment guide : http://www.adacore.com/knowledge/technical-papers/implementa... ) but it would allow so much more code to be SPARK-compatible. Even in the embedded space sometimes you need pointers and linked-lists and hashmaps (and the new formal containers don't do it for you)... Frama-C allows (and seems to work with) pointers, I don't know how Well.

For Ada you can already go a long way (memory safety and data races) with protected object (nice semantics, check performance), not null pointers, controlled-types... But we're far from Rust's borrow-checker and move semantics. The name Unchecked_Deallocation (to instantiate 'Free') says it all.

Can't wait to see some progress on this !