45 ms·

Incidentally, Rust does have an ISO 26262 qualified compiler, though DO-178C isn't here just yet.

MaxBarraclough 1y ago
Doesn't Rust lack a serious language specification? How can compilers be certified without a definitive record of how the language is meant to behave?
- steveklabnik 1y ago
  A language specification is not required to be qualified. The behavior of the compiler needs to be described. https://rust-lang.github.io/fls/ https://rust-lang.github.io/fls/ This is effectively a fork of the Rust Reference, made by Ferrous, and laid out in a way that allowed the compiler to be qualified. It now lives at this URL, because it's being adopted by upstream as the spec.
  - MaxBarraclough 1y ago
    Sounds like progress is being made on the language spec front, that's good to see. I'm not following what you meant by this though, it seems like a contradiction: > A language specification is not required to be qualified. The behavior of the compiler needs to be described. But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language?
    - steveklabnik 1y ago
      > to enable certification It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases. You’re always going to need to have more than a language spec because you qualify compilers not languages. > Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. It has. At least to the degree that regulators find it acceptable. > Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language? There is no difference in flavors, but it is true that each version of the spec is for a specific version of the compiler, and so sometimes that will lag a bit. But that’s just how this process works.
      - MaxBarraclough 1y ago
        Thanks for the reply. Interesting developments for the language.
      - eggy 1y ago
        I considered two things when choosing SPARK2014 over Rust: field-proven legacy apps and a language spec tied to the tooling AND the compiler. A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec.
        steveklabnik 1y ago
        > A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec. I don’t understand. That’s a requirement for qualification.
        eggy 1y ago
        Yes, but a qualified compiler is but one of many pieces in having an ecosystem/tooling for creating, testing, and having high-integrity applications reviewed and certified. A couple of the industries we are elbowing in on, are already familiar with the type of reports generated by the AdaCore tooling. Ada has a decades-long history in safety-critical systems (e.g., Boeing, Airbus, NASA), with proven reliability in real-time, embedded applications. AdaCore’s GNAT Pro suite includes qualified tools (e.g., GNAT Pro, CodePeer, GNATcheck) that support traceability, code coverage, and certification evidence for standards like MISRA, DO-178C, and EN 50128. These are battle-tested in aerospace, defense, and medical applications. Ada is defined by an ISO standard, specifically ISO/IEC 8652. The latest revision, as of 2025, is Ada 2022 (ISO/IEC 8652:2023), which includes updates to the language features. Ada is also recognized as an ANSI standard through its adoption by the American National Standards Institute, aligning with the ISO specification. The standard defines the language’s syntax, semantics, and features, ensuring consistency across implementations including compilers. Rust’s safety guarantees prevent many runtime errors, but its approach relies more on programmer discipline vs. Ada/SPARK2014's "correct by construction" methodology. Ada is designed for real-time systems, with built-in features like tasking, protected objects, and precise control over timing (e.g., Ravenscar profile), optimized for cyber-physical systems. Excuse my verbosity, but I pulled a few things from our tech pitch deck, and a little of the above is in our business plan as well that I copy/pasted. Two great books if you're interested: Analysable Real-Time Systems: Programmed in Ada (2016) Building High Integrity Applications with SPARK (2015)
eggy 1y 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.
- steveklabnik 1y 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.
  - eggy 1y 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.

Doesn't Rust lack a serious language specification? How can compilers be certified without a definitive record of how the language is meant to behave?

steveklabnik 1y ago
A language specification is not required to be qualified. The behavior of the compiler needs to be described. https://rust-lang.github.io/fls/ https://rust-lang.github.io/fls/ This is effectively a fork of the Rust Reference, made by Ferrous, and laid out in a way that allowed the compiler to be qualified. It now lives at this URL, because it's being adopted by upstream as the spec.
- MaxBarraclough 1y ago
  Sounds like progress is being made on the language spec front, that's good to see. I'm not following what you meant by this though, it seems like a contradiction: > A language specification is not required to be qualified. The behavior of the compiler needs to be described. But they're putting work into reviving the language spec, to enable certification? Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language?
  - steveklabnik 1y ago
    > to enable certification It has already been qualified. Upstream has always wanted a spec. It’s being worked on because it’s desirable, not because it’s blocking safety critical cases. You’re always going to need to have more than a language spec because you qualify compilers not languages. > Also, if the source language hasn't been described, then surely the compiler's behaviour hasn't been described. It has. At least to the degree that regulators find it acceptable. > Or did you mean that their documentation is for the Ferrous flavour of Rust and might not reflect the latest version of the Rust language? There is no difference in flavors, but it is true that each version of the spec is for a specific version of the compiler, and so sometimes that will lag a bit. But that’s just how this process works.
    - MaxBarraclough 1y ago
      Thanks for the reply. Interesting developments for the language.
    - eggy 1y ago
      I considered two things when choosing SPARK2014 over Rust: field-proven legacy apps and a language spec tied to the tooling AND the compiler. A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec.
      - steveklabnik 1y ago
        > A qualified compiler doesn't speak to the tooling built around it and how those need to be tied to the spec. I don’t understand. That’s a requirement for qualification.
        eggy 1y ago
        Yes, but a qualified compiler is but one of many pieces in having an ecosystem/tooling for creating, testing, and having high-integrity applications reviewed and certified. A couple of the industries we are elbowing in on, are already familiar with the type of reports generated by the AdaCore tooling. Ada has a decades-long history in safety-critical systems (e.g., Boeing, Airbus, NASA), with proven reliability in real-time, embedded applications. AdaCore’s GNAT Pro suite includes qualified tools (e.g., GNAT Pro, CodePeer, GNATcheck) that support traceability, code coverage, and certification evidence for standards like MISRA, DO-178C, and EN 50128. These are battle-tested in aerospace, defense, and medical applications. Ada is defined by an ISO standard, specifically ISO/IEC 8652. The latest revision, as of 2025, is Ada 2022 (ISO/IEC 8652:2023), which includes updates to the language features. Ada is also recognized as an ANSI standard through its adoption by the American National Standards Institute, aligning with the ISO specification. The standard defines the language’s syntax, semantics, and features, ensuring consistency across implementations including compilers. Rust’s safety guarantees prevent many runtime errors, but its approach relies more on programmer discipline vs. Ada/SPARK2014's "correct by construction" methodology. Ada is designed for real-time systems, with built-in features like tasking, protected objects, and precise control over timing (e.g., Ravenscar profile), optimized for cyber-physical systems. Excuse my verbosity, but I pulled a few things from our tech pitch deck, and a little of the above is in our business plan as well that I copy/pasted. Two great books if you're interested: Analysable Real-Time Systems: Programmed in Ada (2016) Building High Integrity Applications with SPARK (2015)

eggy 1y 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.

steveklabnik 1y 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.
- eggy 1y 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.