This Friday is the next instance of our Ada SPARK Office Hours. Proposed topics:
And of course open to any other topics people are interested to talk about.
More detail and links are here: Ada SPARK Office Hours | AdaCore , 10am-11am ET!
Feel free to propose additional topics by commenting on this article. Recording and summary will be posted typically within a week.
I will try to make this one.
If I can’t, I really would like to ask people who work at AdaCore or have used both Ada and Rust about how they compare and contrast when it comes to memory safety.
I’ve been playing around with Ada SPARK a lot more recently since I feel like conceptually SPARK is like Rust’s borrow checker but on steroids. But, as I’ve looked more into it, it seems like SPARK is weaker in some other areas (since SPARK can only be used on certain files in your Ada project, and SPARK assumes things about the external environment that might not necessarily hold true).
I would be interested if anyone has used SPARK to create something that is wholly memory safe and proven to be memory safe from top to bottom (including Ada’s standard library).
Rust can almost do that with its borrow checker, but low level standard library primitives are made using unsafe Rust, and can, in rare cases, lead to memory vulnerabilities if that part of the standard library hasn’t been audited yet.
(though there is an effort to prove rust’s standard library is memory safe, as shown here: GitHub - model-checking/verify-rust-std: Verifying the Rust standard library · GitHub)
Fantastic topic, let’s dig into that!
Hope you can make it, if not, I can start the discussion and you can see the recording.
Thanks for the suggestion!