[eggy]

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]

> 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]

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)

[steveklabnik]

Ah, I thought we were talking about the language, not the broader way it fits into everything else.

I am familiar with all of this stuff :) I think you may be under-estimating Rust a bit. But that’s fine.

Incidentally, you can also get a Rust qualified compiler from AdaCore. I haven’t kept up with what specific standards they’ve qualified it against though.