4 ms·
Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list conta
by dandotway 5y ago
Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
- p_l 5y agoInterestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
- dandotway 5y agoThe SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)