[eggy]

I am excited Rust is heading in this direction. We had to go with SPARK2014/Ada (2022) when we made this decision over a year ago. Rust and its tooling was and is not ready for the safety critical control system we are developing. High-integrity, safety-critical auditors in government and industry are already aware of the types of reports generated by the AdaCore tooling, so this makes less friction in seeking these certifications. We are also hoping the Ironclad Kernel and Gloire OS gain traction. A kernel written in SPARK2014 and fully formally verified and a complementary OS using Ironclad would make it turtles all the way down to our bare metal controller up to the control system application and HMI. I will certainly keep Rust on my radar in the future. Do you have any examples of where Rust is mainly the PL used in a CPS (Cyber-Physical System) that requires this level of integrity and safety? SPARK has applications in avionics and other industries that go back for decades: Typhoon EuroFighter - flight control and mission-critical systems; Harrier GR9 - avionics; UK NATS iFACTS System - safety-critical air traffic control software; LifeFlow Ventricular Assist Device - medical device to support heart function. SPARK was used for its control software, and the list goes on and on.