I always recommend this book, "Building High Integrity Applications with SPARK" as an introduction to how SPARK can be used for high-integrity, safe programs for mission-critical applications. SPARK has a legacy of large, high-integrity applications over the past two decades. This puts it ahead of Rust in real-world usage for such applications. SPARK2014 the latest, is a formally verified PL along with verification tools/ecosystem made for these type of uses.

I am trying to write show control software in SPARK2014 at the moment. Show control are critical since it is used to power lifts and stage machinery as well as performer flying systems where safety and high-integrity software is critical. I like Rust, but I feel it is not quite there yet especially in terms of the number of real-world systems in this niche. I also find SPARK2014 easier to write and read. I have been programming since 1978, and although I gravitate towards terse, functional languages like Haskell, APL/BQN/J, I experience a lot of friction whenever I dive back into Rust. SPARK2014 is very verbose and Pascal-like, but this is tedium vs. confusion or confidence in what I am writing. I know AdaCore is working with Ferrous Systems to bring Rust more up to the features of Ada/SPARK2014, but for now I needed to make a pragmatic choice based on real-world usage and ease of use and understanding.