I still play with Rust (and Zig), but I have decided to put my work efforts into SPARK[1], the subset of Ada, for high-integrity software and formal verification. I know AdaCore and Ferrous Systems are collaborating in trying to bring a lot of Ada/Spark's capabilities to Rust, but this is still going to be some time. Ada has a longer legacy in this game.
I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada.
This book[2], "Building High Integrity Applications with SPARK" really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any critical mission software written in Rust yet especially that far back.
I found Julia's selection for a flight collision avoidance system perplexing[3], but it proves a PLs syntax and evangelism (maybe not in this case), can bias a selection of a PL for such tasks.
People find Ada/SPARK's syntax and methods verbose and similar to Pascal or other PLs, however, I was up and running quickly in it as opposed to Rust.
You can program to bare metal in SPARK, and the tools are already there to provide high-integrity software. The tools for SPARK automate most of the verification. Most of Rust's wishlist is already in SPARK (and Ada). I hope the Ferrous Systems and AdaCore collab bears fruit for Rust, but I have been programming since 1978, and I play with many PLs, but I found Rust's initial learning curve very off putting and I don't have the time to wait for it to mature to SPARK's level. And this is from someone who loves J/APL/BQN and Lisp, so I have no issue with different programming paradigms. I found Zig much easier to get things done from the start, although it does not strive to be a SPARK or Rust.
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!)
Regarding the collaboration between AdaCore and Ferrocene, the effort is to produce a Rust toolset that is qualified for safety critical usage (e.g. verification of object code that is produced, etc). That is _not_ the same as bringing SPARK-like language capabilities to Rust. I think too many people get that confused.
I've looked a tiny bit into Ada and I like the language. I particularly like the pascal-like syntax and the ranges feature.
However I love rusts cargo and build system better than Alire. As Alire seems to bolted ontop of gprbuild. I also find it unfun to go back to forward declaration and definition (ads) files.
It also seems to me the rust ecosystem has more libraries in things I'm interested in and better support for the platforms I'm interested in.
What libraries are you interested in that Rust has and other PLs do not?
What is your main use of Rust? It all depends on what you are doing. I use Zig for fun game dev stuff, and not SPARK, but for the safety-critical control systems, it's SPARK, not Zig or Rust.
I'm using rust to develop a internet client. So I need libraries for gui; rust has many to choose from (I'm using gtk currently). I see a few that plan on supporting Android which I'd like to port to down the line. Of course rust has many networking libraries also so I feel covered there.
Safety is fairly important and I like ada/spark for that but rust's community seems to be farther along in terms of support for Android and looks way more active right now.
what resources can you suggest to learn formal verification and implement it to make high integrity fault tolerant services? I am quite intrigued by AdaCore. Want to try it out. I dont know much about Formal Verification.
I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada.
This book[2], "Building High Integrity Applications with SPARK" really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any critical mission software written in Rust yet especially that far back.
I found Julia's selection for a flight collision avoidance system perplexing[3], but it proves a PLs syntax and evangelism (maybe not in this case), can bias a selection of a PL for such tasks. People find Ada/SPARK's syntax and methods verbose and similar to Pascal or other PLs, however, I was up and running quickly in it as opposed to Rust.
You can program to bare metal in SPARK, and the tools are already there to provide high-integrity software. The tools for SPARK automate most of the verification. Most of Rust's wishlist is already in SPARK (and Ada). I hope the Ferrous Systems and AdaCore collab bears fruit for Rust, but I have been programming since 1978, and I play with many PLs, but I found Rust's initial learning curve very off putting and I don't have the time to wait for it to mature to SPARK's level. And this is from someone who loves J/APL/BQN and Lisp, so I have no issue with different programming paradigms. I found Zig much easier to get things done from the start, although it does not strive to be a SPARK or Rust.
[1] https://www.adacore.com/sparkpro
[2] https://www.amazon.com/Building-High-Integrity-Applications-...
[3] https://juliahub.com/case-studies/lincoln-labs/