I know Rust has many goals on paper that align with this decision, however, what large codebases in the field of high-integrity software are written in Rust? Do

I know Rust has many goals on paper that align with this decision, however, what large codebases in the field of high-integrity software are written in Rust? Does Rust comply with high-integrity software standards (CENELEC EN 50128, DO-178C,DEFSTAN 00-56, or IEC 61508) in any capacity? SPARK2014 has been around much longer, does comply with those standards, is a formally defined PL with a great set of verification tools specifically designed for high-integrity software. There are large codebases (software for the safe operation of helicopters at sea (27k LOC of SPARK2014); NATS iFACTS air traffic control system (>529K LOC of SPARK2014). I am glad that AdaCore is teaming up with Ferrous Systems to help bring some of Ada and SPARK's goodies to Rust, but it's nowhere near them at this point. This seems more a Rust champion at Volvo convinced their group to use it. >>>JG: Then I pitched to the managers, “If we want to do a serious Rust effort within the company, then I want to take part in that and become an employee”, since I was a consultant at that point. The availability of programmers in either Rust or SPARK2014 shouldn't be a heavily weighted factor, since anyone working in SPARK2014 probably already has the relevant experience no matter how few apply, whereas the dozens or more of Rust programmers who might like working at Volvo would be cutting their teeth trying to build 1/20 of what Ada/SPARK2014 already have, and possibly deliver far less. Rust is to C++ as SPARK2014 is to Rust at this point in my opinion, but current popularity wins out a lot in all human endeavors. I'll stick with SPARK2014 and Zig for now until Rust catches up SPARK2014.