Hacker News new | ask | show | jobs
by eggy 338 days ago
That's for automotive. We're shooting for a bunch of various relevant standards. There is no formal language spec. Who did that compiler? AdaCore's been around for a long time, so I am quick to use theirs if I were to chose Rust. I'm also following the Ironclad kernel project with its complementary OS called Gloire. Ada/SPARK for both with partial formal verification progress.
1 comments
steveklabnik 338 days ago
Automotive is the first industry that’s really taking up Ferrocene! They’re adding more stuff as more industries have demand for it.

Ferrous and AdaCore were originally collaborating, but then they parted ways. In my understanding they’re both largely the upstream codebase, I know that the Ferrous folks religiously upstream almost everything, no clue if AdaCore does as well.

link
eggy 333 days ago
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.
link