SPARK: Rust inspired adding of pointers to formal verification language


#1

It’s great to see that Rust is spurring on language innovation. SPARK is a formal subset of Ada and it appears they are looking to extend the expressiveness of the language by adding in Rust-like aliasing.

(I’m not related to the project, just found it interesting)


#2

@gilescope Just a nit. As one of the people who developed Green, which was selected by the US DoD to become Ada, the language name is “Ada” – the given name of the woman considered to be the world’s first programmer. The language name is not the acronym “ADA”.


#3

Corrected - I hope she will forgive me! - It was SPARK that should have been in capitals.