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)
@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".
Corrected - I hope she will forgive me! - It was SPARK that should have been in capitals.