The SPARK teams at AdaCore & Altran UK are working hard right now to bring proved memory safety, some kind of borrow-checker to SPARK (and then hopefully, Ada).

The SPARK teams at AdaCore & Altran UK are working hard right now to bring proved memory safety, some kind of borrow-checker to SPARK (and then hopefully, Ada). I think they have something working already but they want it to work in an industrial, high integrity context, so : for every case, all the time, with minimum training and complexity for the developer. Amazing what a small team of clever, focused people can achieve. By the way, it's great that Rust is starting to get 'formal-proof' interest, but I fear they're starting on a path without looking at the experience of others. I'm thinking about creating an adhoc language to write properties, pre-/post- conditions, etc. The power of SPARK2014 is in big part the result of Ada2012 integrating executable contracts /written directly in Ada/. This enables so much ! Lower learning curve, the ability to transition smoothly from Ada to SPARK bronze (every variable is always initialized before use, no aliasing...), silver (absence of runtime errors and since Ada comes with tons or runtime checks, that's amazingly safe already), gold (prove some Properties, kind of the PBT of proof :-) ), platinum (full specification, proved) levels... At the very least, now you have contrats in Ada, you can improve your interfaces. Where typing wasn't enough to express semantics, contacts can help. If you've written properties/contracts, now you can verify them with SPARK or if too hard, test it, fuzz it... I also hope they'll look into why3 and all the amazing work that's been done to help abstract over SMT solvers, and allow to play on each solver's strength ! Alt-ergo, cvc4, z3... It would be great for all 'safe' languages (SPARK2014, Frama-C, Java/JML, now rust) to share some common good base layers for proof. I know there's a lot of collaboration and cross-pollination between the Frama-C and SPARK2014 worlds.