I totally agree. In reality, today, if you want to produce auditable high-integrity, high-assurance, mission-critical software, you should be looking at SPARK/Ada and even F* (fstar). SPARK has legacy real world apps and a great eco system for this type of sofware. F* is being used on embedded and in other realworld apps where formal verification is necessary or highly advantageous. Whether I like Rust or not, should not be the defining factor. AdaCore has a verifed Rust compiler, but the tooling around it does not compare to that around SPARK/Ada. I've heard younger people complain about PLs being verbose, boring, or not their thing, and unless you're a diehard SPARK/Ada person, you probably feel that way about it too. But sometimes the tool doesn't have to be sexy or the latest thing to be the right thing to use. Name one Rust realworld app older than 5 years that is in this category.
> Name one Rust realworld app older than 5 years that is in this category.
Your "older than 5 years" requirement isn't really fair, is it? Rust itself had its first stable release barely 10 years ago, and mainstream adoption has only started happening in the last 5 years. You'll have trouble finding any "real-world" Rust apps older than 5 years!
As to your actual question: The users of Ferrocene[0] would be a good start. It's Rust but certified for ISO 26262 (ASIL D), IEC 61508 (SIL 4) and IEC 62304 - clearly someone is interested in writing mission-critical software in Rust!
The point was how would you justify choosing Rust based on any real world proof. Maybe it will be ready in a few years, but even then it is far from achieving what you already have in SPARK along with proven legacy. I am very familiar with this, and I still chose SPARK/Ada instead of Rust. SPARK is already certified for all of this. And aerospace, railway, and other high-integrity app industries are already familiar with the output of the SPARK tools, so there's less friction and time in auditing them for certification. Aside from AdaCore, who collaborated with Ferrocene, to get a compiler certified I don't see much traction to change our decision. We are creating show control software for cyber-physical systems with potential dire consequences, so we did a very in-depth study Q1 2025, and Rust came up short.
