Every Rolls-Royce gas turbine FADEC runs ADA binaries on a custom processor [1].
It's also used extensively at Airbus. Lots of DO-178C (safety critical aerospace).
1: https://www.his-conference.co.uk/session/visiumcore-a-high-i...
The Ada mandate for mission-critical software was only in place from 1991-1997.
https://www.ghs.com/products/ada_optimizing_compilers.html
https://www.ptc.com/en/products/developer-tools/apexada
https://www.ddci.com/products_score/
http://www.irvine.com/tech.html
"NVIDIA began implementing SPARK in its security strategy in 2019 on select pieces of firmware. They began training additional personnel in SPARK and eventually developed an in-house training program.
Several NVIDIA teams are now using SPARK for a wide range of applications that include image authentication and integrity checks for the overall GPU firmware image, BootROM and secure monitor firmware, and formally verified components of an isolation kernel for an embedded operating system, to name just a few."[0]
https://www.adacore.com/nvidia
[0] https://www.wevolver.com/article/nvidia-adoption-of-spark-us...
> NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.
Ada’s strictness about types and a preference to allocate on the stack rather than the heap means more bugs are caught at compile time. Claude Code is really good at iterating on compile time errors without much user intervention.
While the amount of source code written in assembly languages is an extremely small fraction of the total existing code and only few programmers are competent to write such programs, that assembly source code determines a large fraction of the performance of the applications run on modern computers.
LLMs are likely to behave similarly, i.e. a good amount of programs will continue to be written directly in deterministic programming languages by competent programmers, while a greater amount of source code, usable for solving problems that are neither novel nor critical, will be generated by people with lower skills, with the help of LLMs.
I'm pretty sure these aren't big issues these days, but there's still a lot of people walking around thinking "I can't use Ada on this project, I don't have budget for a commercial compiler." Maybe a "project manager's introduction to Ada." I would write it myself, but I've forgotten most everything I learned about the language and it's development community.
[Apart from that... young engineers should definitely check out Ada, even if you don't eventually use it. Why it was considered a good idea to create a new language, the problems language designers were trying to solve and how developers used the language to build code that was more bullet-proof than C++ is kind of an interesting story.]
All Ada language features are present in the free/open source version of the compiler. The proprietary version of GNAT is just updated more frequently I think and has commercial support - they periodically copy their changes into the main GCC source tree.
They have proprietary tools for some kinds of static analysis, but those wouldn’t be considered language features. GNATprove (the theorem prover tool for verifying SPARK programs) is open source.
https://blog.adacore.com/a-new-era-for-ada-spark-open-source...
https://zaguan.unizar.es/record/79726/files/texto_completo.p...
AdaCore does directly contribute to GNAT which is important.
GNAT was chosen for alire since it is free software: "This work presents a working prototype tailored to the Ada compiler available to open source enthusiasts, GNAT."
Other Ada implementations typically use their own build systems which are different from GNAT's and so they would probably need changes to work with alire.
At this point it is becoming the de facto method of acquiring the toolchain and building Ada projects.
I never heard about Spark/Ada before. I wonder if anyone uses Spark for real world tasks, and if yes, what for?
https://en.m.wikipedia.org/wiki/High-integrity_software
A well known user is NVidia, and car industry security standards.
https://www.adacore.com/press/ada-and-spark-enter-the-automo...
eggy•5mo ago