Hacker News Reader

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').

View on HN

Interestingly 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.

The 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-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. :-)

Reply on news.ycombinator.com