My understanding is that Rust doesn't have so much to offer Ada/SPARK. I haven't looked that hard at Rust though, so maybe I've overlooked some of it's features.
You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety.
Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees.
Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though.
I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.
You have to jump through the same sort of hoops in Rust as you do C++ to get the sort of basic type safety found in Ada/SPARK. Rust doesn't so much have a focus on safety and correctness in general, as a focus on memory safety.
Admittedly, Ada/SPARK doesn't make the kinds of guarantees that Rust does about memory. However, accessibility checks help prevent dangling pointers and the use of memory subpools can avoid the need for explicit frees.
Additionally, Ada offers some features like the ability to return a dynamically sized array as if it were on the stack which helps reduce how often memory needs to be manually managed. I believe SPARK may not allow this sort of thing though.
I'm also not sure why you would want to abandon the actually verified properties of Ironsides for a hope those properties remained in an unverified port.