In this article I talk a little bit about safe programming language, and why they’re so important. I cover what is considered to be the safest programming language developed.
A language where if the program is brought to a failed/invalid state, it could potentially cause the loss of one or more human lives, and/or hundreds of millions of pounds in assets (an Ariana 5 will set you back about $180 million without payload, $700m-$1 billion with).
Disclaimer: this is purely from a weekend of sporadic research, reading a few blogs from engineers in that field, and making a few hello world level programs. I’m prefer higher level programming, but this was just too interesting to forget about.
Rust has made a massive splash since its initial release in 2012, effectively one-upping C++ by proving protections against memory safety errors and data races with its borrow checker. This is inline with the state of software development today, and shows the industry’s trend towards safer languages, specifically low-level system languages.
In 2024, the United States White House Office of the National Security Director (mouthful) released a report urging software development to move away from unsafe languages like C and C++ to memory safe alternatives.
So today, I’d like to explore one of the safest languages I’ve been reading about lately. A language where, supposedly, it is mathematically impossible to enter a failed/error state. A language where if it does enter an error state, one or more human lives could be lost.
Named after an English mathematician, and the first ever computer programmer, Ada Lovelace.
Ada (and SPARK)
So here’s what I’ve gathered so far. Ada came first, it’s the actual programming language that’s used. Originally specified in MIL-STD-1815, Ada 83 was created by Jean Ichbiah for Honeywell (now Bull SAS), under contract with the United States Department of Defense (now the Department of War?). The syntax reminds me of Pascal. If you haven’t seen it before, it looks like this (from Wikipedia)
with Ada.Text_IO;
package body Example is
i : Number := Number'First;
procedure Print_and_Increment (j: in out Number) is
function Next (k: in Number) return Number is
begin
return k + 1;
end Next;
begin
Ada.Text_IO.Put_Line ( "The total is: " & Number'Image(j) );
j := Next (j);
end Print_and_Increment;
-- package initialization executed when the package is elaborated
begin
while i < Number'Last loop
Print_and_Increment (i);
end loop;
end Example;Ada vs SPARK: What’s the relationship?
This part confused me at first, so let me try to explain what I’ve come to understand. Ada and SPARK are related, but they’re not the same thing. You might hear people say “Ada SPARK” as if it’s one language, but that’s a bit misleading.
Ada is a full programming language, designed for safety-critical and embedded systems. It has strong typing, built-in concurrency, and a lot of features that help catch bugs at compile time. You can write perfectly valid Ada code that does all sorts of things, including things that are hard to formally verify.
SPARK is a formally defined subset of Ada. All SPARK code is valid Ada code, but not all Ada code is valid SPARK code. Think of it like this: if Ada is the full language, SPARK is Ada with some features deliberately removed or restricted. The SPARK tools (like GNATprove) can then analyse this restricted subset and mathematically prove properties about your code.
Why take features away instead of adding them? Because formal verification is hard. Really hard. And some language features make it mathematically impossible to prove correctness.
Think about pointers in C. How do you prove a pointer isn’t going to segfault without tracking every possible memory state? You can’t, really. So SPARK bans unrestricted access types (Ada’s equivalent of pointers). Want dynamic dispatch with polymorphism? That makes static analysis a nightmare when you’re trying to prove execution paths at compile time, so that’s gone too. Exception handling that jumps around unpredictably makes it impossible to reason about program state, so that’s limited as well.
The entire philosophy seems to be: if we can’t prove it’s safe with mathematical certainty, you’re not allowed to use it. It’s not about making programming easier or more productive, it’s about making it provably correct. That’s why it’s a subset. They’re not adding features, they’re removing anything that breaks the proof system.
SPARK has evolved alongside Ada, with versions like SPARK83, SPARK95, and SPARK2005 corresponding to their respective Ada versions. The current version, SPARK 2014, builds on Ada 2012 and integrates contracts directly into the language syntax using aspects like Pre, Post, and Ghost.
So where is Ada and SPARK used?
From what I’ve been researching, the usage is extensive. Many NATO countries mandate that systems involving command and control functions are written in Ada. Ada is apparently in the Eurofighter Typhoon, JAS 39 Gripen, F-22 Raptor and the F-14 Tomcat.
On the Victoria Line in London, there is a system called the Automatic Train Operation (ATO). The core is written in Ada, and the emergency braking systems are in SPARK. This was adapted to the Taipei Metro as well.
UK iFACTS (Interim Future Area Control Tools Support) is a next generation Air Traffic Control system implemented in Ada and SPARK.
The French high-speed TVM in-cab signalling uses Ada.
The Ariane 4 and 5 space rocket flight control systems are Ada. Various satellite and space systems are Ada and/or SPARK. The Canadarm2 on the International Space Station is GNAT Ada 95.
And that’s just cracking the surface. Medical devices, banking and financial systems, industrial automation, the energy sector, manufacturing, telecoms and networking, public infrastructure and voting systems, engineering and CAD, and security critical systems all use these languages.
This is where code cannot go wrong.
Digging Into SPARK
That’s enough of a high level overview for this article. Let’s dig a bit deeper into SPARK specifically and see how it actually works.
From what I understand, we can make code that has preconditions and postconditions, which is fed into a prover during the compilation steps. This proves the subprogram cannot fault.
Here’s a simple example of what that looks like
function Increment (X : Integer) return Integer
with Pre => X < Integer'Last,
Post => Increment'Result = X + 1
is
begin
return X + 1;
end Increment;The Pre and Post aspects are contracts. The precondition says "X must be less than the maximum integer value", preventing overflow before it happens. The postcondition says "the result will be exactly X + 1". GNATprove will analyse this and either prove these contracts hold for all possible inputs, or tell you exactly where they could fail.
But it goes deeper. You can specify invariants, type predicates, and flow dependencies. Here’s something closer to a real safety-critical system
package body Brake_Controller
with SPARK_Mode
is
type Brake_Pressure is range 0 .. 100; -- 0 to 100 PSI
type Speed is range 0 .. 200; -- 0 to 200 mph Current_Pressure : Brake_Pressure := 0;
function Calculate_Brake_Pressure
(Current_Speed : Speed;
Target_Speed : Speed)
return Brake_Pressure
with
Pre => Current_Speed >= Target_Speed,
Post => Calculate_Brake_Pressure'Result <= 100
is
Speed_Difference : Speed := Current_Speed - Target_Speed;
begin
if Speed_Difference > 100 then
return 100; -- Max pressure
else
return Brake_Pressure(Speed_Difference);
end if;
end Calculate_Brake_Pressure;
procedure Apply_Brakes
(Current_Speed : Speed;
Target_Speed : Speed)
with
Pre => Current_Speed >= Target_Speed,
Post => Current_Pressure <= 100
is
begin
Current_Pressure := Calculate_Brake_Pressure(Current_Speed, Target_Speed);
-- In real code, this would interface with hardware
end Apply_Brakes;
end Brake_Controller;
When you run GNATprove on this, it will verify that the pressure can never exceed the physical limits (0–100 PSI), that subtraction operations can’t underflow, that all type constraints are maintained, and that the postconditions are guaranteed to hold if the preconditions are met.
If you tried to call Apply_Brakes(50, 75) (braking while going slower than target), GNATprove would flag that as a contract violation at compile time. The code wouldn't even build.
How the proof system actually works
SPARK bans features that break our ability to analyse (things like unrestricted pointers, aliasing, and so on) and enforces a stricter subset of Ada. By statically analysing the code, the proof tools (like GNATprove) can prove that buffer overflows cannot exist, that integer overflows cannot exist, that no data races can exist, and that the contract specifications (pre/postconditions and invariants) are correct.
The proof system uses SMT solvers (like Alt-Ergo, CVC5, and Z3) under the hood. You write contracts, SPARK generates verification conditions (mathematical formulas), and the solvers attempt to prove them. If they succeed, you have mathematical proof your code is correct. If they fail, you get a counterexample showing exactly how your code could break.
A practical example: Building a ring buffer
Let’s build something you might actually use, a bounded ring buffer. From what I’ve read, this is common in embedded systems and safety-critical applications because it has predictable memory usage and no dynamic allocation.
package Ring_Buffer
with SPARK_Mode
is
type Buffer_Index is range 0 .. 15; -- 16 element buffer
type Element is new Integer;
type Buffer_Array is array (Buffer_Index) of Element; type Ring_Buffer is record
Data : Buffer_Array := (others => 0);
Head : Buffer_Index := 0;
Tail : Buffer_Index := 0;
Count : Natural range 0 .. 16 := 0;
end record;
function Is_Full (Buffer : Ring_Buffer) return Boolean is
(Buffer.Count = 16);
function Is_Empty (Buffer : Ring_Buffer) return Boolean is
(Buffer.Count = 0);
procedure Push
(Buffer : in out Ring_Buffer;
Item : Element)
with
Pre => not Is_Full(Buffer),
Post => not Is_Empty(Buffer)
and Buffer.Count = Buffer.Count'Old + 1;
procedure Pop
(Buffer : in out Ring_Buffer;
Item : out Element)
with
Pre => not Is_Empty(Buffer),
Post => Buffer.Count = Buffer.Count'Old - 1;
end Ring_Buffer;
The body
package body Ring_Buffer
with SPARK_Mode
is
procedure Push
(Buffer : in out Ring_Buffer;
Item : Element)
is
begin
Buffer.Data(Buffer.Tail) := Item;
Buffer.Tail := (Buffer.Tail + 1) mod 16;
Buffer.Count := Buffer.Count + 1;
end Push; procedure Pop
(Buffer : in out Ring_Buffer;
Item : out Element)
is
begin
Item := Buffer.Data(Buffer.Head);
Buffer.Head := (Buffer.Head + 1) mod 16;
Buffer.Count := Buffer.Count - 1;
end Pop;
end Ring_Buffer;
Run GNATprove on this and it would verify that array accesses are always in bounds, the count never exceeds 16, Push and Pop maintain the ring buffer invariants, the modulo arithmetic never causes issues, and the postconditions hold.
If you tried to remove the not Is_Full(Buffer) precondition from Push, GNATprove would fail with "overflow check might fail" because Count + 1 could exceed 16. The proof system forces you to handle that edge case.
Why this matters (and why you probably don’t need it)
Let’s be real: most of us are building web apps, internal tools, or services where a crash is annoying but not catastrophic. You don’t need SPARK for your Next.js dashboard or your Python ETL script. The overhead isn’t worth it.
But if you’re writing code where failure means a plane doesn’t land correctly, a medical device gives the wrong dose, a train doesn’t stop in time, a spacecraft drifts off course, or a nuclear reactor doesn’t shut down safely, then SPARK makes sense. It’s the difference between “we tested this extensively” and “we proved this mathematically cannot fail in these specific ways.”
The trade-off is development velocity. Writing SPARK is slower. Proving your code is slower. Debugging proof failures is painful. You’ll spend hours tweaking contracts to satisfy the proof system. But when human lives depend on your code, that’s a trade-off worth making.
The learning curve and tooling
I’m not going to sugarcoat it, the learning curve is steep. Ada itself has a learning curve if you’re coming from C-like languages, and SPARK adds another layer on top. You need to understand Ada’s type system and contracts, how proof systems work, how to write provable code (which is different from normal code), and how to debug proof failures (which are often cryptic). And I’ll be honest here, I’ve barely scratched the surface and still barely understands how it all works.
The tooling is… fine. GNAT Studio (the IDE) is seems functional but not VSCode or IntelliJ level of polished. GNATprove is CLI first. The documentation is comprehensive but a little dense. There’s no massive ecosystem of libraries like Nuget, npm, PyPI.
But the communities (Ada and SPARK) are small and seem genuinely helpful. If you ask a question on the Ada subreddit or the SPARK forums/Discord servers, you’ll get thoughtful responses from people who genuinely care about the language and its use cases.
Rust vs SPARK: A quick comparison
Rust gets a lot of attention for memory safety, and rightfully so. But Rust and SPARK solve different problems.
Rust focuses on memory safety at compile time, thread safety through ownership and borrowing, zero-cost abstractions, and practical systems programming. SPARK, on the other hand, focuses on mathematical proof of correctness, formal verification of contracts, absence of runtime errors (proven, not just caught), and safety-critical certification (DO-178C, IEC 61508, and so on).
Rust prevents entire classes of bugs through clever language design. SPARK proves mathematically that specific bugs cannot exist. Rust is great for building fast, safe systems software. SPARK is great for proving your aircraft won’t fall out of the sky.
You can use both. Some projects use Rust for the fast, modern parts and Ada/SPARK for the safety-critical core. They’re not competitors, they’re tools for different problems.
Safety at a cost
Ada and SPARK represent the extreme end of software correctness. It’s not about writing code that probably works or usually doesn’t crash. It’s about mathematical proof that specific failure modes cannot exist.
The cost is high: slower development, steeper learning curve, limited ecosystem, more restrictive language features. But when the alternative is literal loss of life, that cost becomes acceptable.
If you’re building a web app, stick with TypeScript or Rust or whatever you’re comfortable with. But if you ever find yourself working on code where failure is genuinely catastrophic, remember that SPARK exists. It’s a tool built for a specific purpose: making it impossible (not just unlikely) for certain bugs to exist.
And honestly? Even if you never write a line of SPARK, learning about it will make you a better programmer. It’ll change how you think about preconditions, invariants, and what it really means for code to be “correct.” That’s valuable regardless of what language you’re writing.