I'd say most of the truly safety critical control code I encounter was generated in simulink, and the remainder is all in subsets of c++. Some of that c++ was loosely ported from ada (not spark) long ago. So rust wouldn't be taking over the domain from spark, it would be taking it over from c++ and simulink which took over half of the safety critical domain some years ago, many years if you count misra c. I would certainly advocate for spark over any of those languages, but that is a hard sell as people want free open source tooling that is used by google or amazon, and if they say no to spark, but yes to rust, well at least it isnt c++98 anymore. Or simulink models version controlled using folders with dates in the names.
SPARK being a derivative of Ada, which appeared over 40 years ago, inherits its legacy, so I would say it is older than its 2014 name tag. It was based on the Ada 2012 specification. Contracts are relatively new, but it has many real world mission critical applications in its portfolio other than the CubeSat program I put forth from 2013[2]. Rust wasn't even two years old at that point.
If you go back, then assembly was mainly used in mission critical software in aerospace, for example the Apollo guidance system. To quote an article about NASA programmer, Ron Garret about options in 1988[1] and the now-famous Lisp troubleshooting from 150 million miles away:
“There is Pascal and C and Basic and machine code. And that’s pretty much it in terms of popular languages. To get anything done in any of those languages is just really, really hard.” The code for most spacecraft ended up being written in assembly language.
I want free too, but tooling makes the system, and in SPARK2014 it is the tooling, not just the formally verified spec. of the PL that makes it really groove. Rust has a great build system in Cargo, but it does not have 10% of what SPARK2014/Ada/GNAT provide as an ecosystem and apps under its belt. I do think there are people working on this for Rust (Ferrous Systems with AdaCore), but I want to ship a product before that will ever happen. Maybe my next project will be Rust or Zig with contracts or April (Lisp and APL - my favorite, although there is BQN implemented in Rust!)
