People have picked stranger things than julia for safety critical control systems. I know people have generated it from simulink and have used labview, and it wouldn't surprise me if somewhere someone is using an excel macro to control the pressure system on a boiler... The world is a scary place.
Reading theough the spark tutorials and examples seems fairly similar to the rustlings excercise. I find the ways spark prevents problems, like forbidding side effects, is more onerous than the borrow checker making me specify a lifetime every so often. I'm not saying you are wrong to prefer spark, just that people with different backgrounds will find the learning curves different. You have been programming longer than I've been alive, so you certainly have a different perspective. I started with c64 basic then c on the amiga 500, then x86 assembler on 386, them turbo pascal, then turbo c++ on the 386.
I can't argue that spark isn't more mature for formal verification, but it feels like formal verification relies heavily on correct contract specifications with no way to measure when your contracts are correct. Unit tests and coverage at least give me a little feel good that I wrote enough tests for my rust.
I started working with functional safety only two years ago, and I've been surprised when colleagues expressed that Simulink was actually the go-to solution for functional safety software where they were working before. The logic being that the Simulink toolchain is qualified for functional safety, and if you use it in combination with a qualified C toolchain and RTOS, then you're good to go, certification-wise.
My impression when working with people using Simulink is that 'safety' is much weaker that for people working on formal methods, and certification limited a lot the kind of programs that they would write. It made totally sense for their domain, but -- as a general practice to write software -- it didn't impress me at all. I may be wrong.
I was expecting functional safety standards to require the use of formal methods, similar for example to how AWS uses TLA+, but I was surprised to discover it was not a requirement at all.
SPARK is expressive and it has a formal specification from the get go that makes it easier to stay within the requirements and provides automatic verification. GNAT tools are pretty cool. I don't think Rust has much of this other than its specification. It has momentum and a great community, so I think either way it will succeed in many endeavors. Like Erlang for distributed computing, I think SPARK has carved out and earned its niche, and Rust will not soon take over this domain.
For me, Rust seems too complicated at this point. I will continue to play and watch it. I use the Helix Editor, which I love, and it is written in Rust!
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!)
Reading theough the spark tutorials and examples seems fairly similar to the rustlings excercise. I find the ways spark prevents problems, like forbidding side effects, is more onerous than the borrow checker making me specify a lifetime every so often. I'm not saying you are wrong to prefer spark, just that people with different backgrounds will find the learning curves different. You have been programming longer than I've been alive, so you certainly have a different perspective. I started with c64 basic then c on the amiga 500, then x86 assembler on 386, them turbo pascal, then turbo c++ on the 386.
I can't argue that spark isn't more mature for formal verification, but it feels like formal verification relies heavily on correct contract specifications with no way to measure when your contracts are correct. Unit tests and coverage at least give me a little feel good that I wrote enough tests for my rust.