Strong types, strong guarantees, and a track record measured in flight-hours.

Introduction: The rumor of obsolescence

Every few months, a viral thread declares a venerable technology “dead.” Ada, designed in the late 1970s and standardized in the early 1980s, is a frequent target. The meme is simple: “Nobody uses Ada anymore.” And yet planes take off, satellites phone home, trains brake exactly when they should, and medical devices dose with extraordinary precision—many using Ada or its formally verifiable subset, SPARK. The language that was engineered for “systems that must not fail” continues to do precisely that: not fail.

This essay is a deep dive into why Ada still matters. It traces Ada’s origins in the Department of Defense (DoD) language consolidation effort, explains its core design (and why those design choices feel uncannily modern), explores real-world deployments (including Boeing 777 avionics and the F-22 Raptor), and unpacks the ecosystem around contracts, verification, and high-integrity software. It also tackles common misconceptions, compares Ada to modern safety-oriented languages like Rust, and closes with a practical guide for curious developers who want to try Ada without wading through a wall of acronyms.

No hype. Just the engineering logic behind a language that keeps quietly doing its job.

1) A language born from the software crisis

In the late 1960s and early 1970s, the DoD faced an untenable situation: vast, long-lived systems written in a chaotic zoo of custom languages, dialects, and macro assemblers. Code had to be certifiable, maintainable for decades, and portable across evolving hardware. Projects were slipping schedules and budgets because the language layer itself amplified complexity.

The DoD’s response was methodical:

From day one, Ada wasn’t trying to be cool. It was trying to be correct.

2) Design philosophy: correctness by construction

Most mainstream languages assume “you’ll be careful,” then provide libraries to patch over foot-guns. Ada flips that: it starts from the assumption that correctness is a first-class requirement, then bakes it into the type system, compilation model, concurrency semantics, and run-time checks.

Key pillars:

If you’ve ever wished your compiler were more like a guardian angel than a permissive roommate, Ada will feel like home.

3) The big revision: Ada 95 and beyond

Ada didn’t stand still. Major milestones:

These steady upgrades targeted correctness, analyzability, and composability—precisely what long-lived, safety-critical codebases need.

4) Real-world deployments: when failure isn’t an option

Boeing 777 avionics (AIMS) The Boeing 777’s Airplane Information Management System (AIMS), often described as the aircraft’s “brains” for information management and integration, has been documented as largely implemented in Ada. That choice isn’t accidental. When software must deliver consistent behavior across millions of flight-hours, languages that encourage explicit constraints, analyzable concurrency, and verifiable behavior are favored.

F-22 Raptor The Lockheed Martin F-22 is widely reported to have a large Ada codebase in its avionics. Again, the fit is obvious: concurrency, timing, deterministic behavior, and a type system that prevents entire classes of errors at compile time—exactly what fighter aircraft software demands.

Air-traffic control, rail, medical Beyond headline aerospace programs, Ada shows up in rail signaling, power systems, air-traffic control consoles, and medical devices—places where rare edge cases are not “interesting bugs” but unacceptable risks.

The common denominator isn’t fashion. It’s certification.

5) SPARK: write code the prover can love

Arguably the most exciting chapter in Ada’s story is SPARK, a formally defined, contract-heavy subset designed for proof. Where Ada’s contracts let you express invariants, SPARK’s toolchain (e.g., GNATprove) attempts to prove them. Not test them—prove them.

What SPARK targets:

The outcome is profoundly pragmatic: software where entire categories of catastrophic failure are ruled out by construction. If testing is sampling, SPARK is a proof that you’re in the right universe.

This is not limited to academics. SPARK has been applied in industrial projects where certification evidence is required (avionics standards like DO-178C, railway EN 50128/50129, automotive ISO 26262 adjacent contexts). The reason is simple: every unit of provability can reduce the cost and risk of certification audits.

6) Concurrency without chaos: tasks, rendezvous, and Ravenscar

Concurrency kills correctness when it’s an afterthought. Ada integrates concurrency at the language level:

For hard real-time use, the Ravenscar profile trims the concurrency model to a minimal, static, analyzable subset: no dynamic task creation at runtime, fixed priorities, no fancy features that complicate worst-case analysis. It’s “just enough concurrency” for schedulability analysis and formal verification.

If your mental model of threads is “mortal enemies fighting over a mutex,” Ada’s approach feels like a peace treaty enforced by the compiler.

7) Contracts and defensive programming that scale

With Ada 2012, contracts became part of everyday programming:

procedure Transfer (From, To : in out Account; Amount : in Money)
  with
    Pre  => (Amount > 0) and (From.Balance >= Amount),
    Post => (From.Balance = From'Old.Balance - Amount)
            and (To.Balance   = To'Old.Balance   + Amount);

Now combine that with SPARK’s proofs and you get a spectrum: runtime checks during testing, proofs for production-critical code, and contracts that double as documentation. You’re not sprinkling comments—you’re enforcing truths.

8) “But isn’t Ada obsolete?”—a myth-busting FAQ

“Nobody uses it.” Incorrect. It remains in active use across avionics, rail, defense, and medical domains. Those industries do not optimize for social-media trends; they optimize for assurance.

“It’s too old to be relevant.” Age only correlates negatively when a language stops evolving. Ada’s standard has continued to grow (95, 2005, 2012, and refinements), keeping its contract model, verification hooks, and real-time features in step with modern safety standards.

“We can just write C carefully.” You can, and many teams do, but “careful” in C often means “expensive process discipline forever.” Ada bakes many checks into the type system and semantics, reducing the number of things teams must remember not to do. SPARK goes further: prove, don’t hope.

“Rust made Ada irrelevant.” Rust and Ada share goals around safety but take different routes. Rust’s ownership model eliminates data races and many memory unsafety bugs without GC; Ada leans on strong typing, contracts, and formal methods (SPARK) for proof-based assurance. In safety-critical certification contexts, Ada/SPARK’s maturity and existing qualified toolchains remain decisive. It’s not either/or; they can coexist, and ideas cross-pollinate.

“You can’t build modern systems with it.” You can. Embedded boards, RTOS targets, mixed-language systems, C/C++ interfacing, even modern build pipelines—with the added benefit that your code is analyzable to a level mainstream stacks rarely achieve.

9) An Ada vs. Rust mental model (without the flame war)

Both are great; each excels in contexts tuned to its philosophy.

10) Idiomatic Ada: a taste of the language

Range-checked numeric types

subtype Percent is Integer range 0 .. 100;

type Celsius is delta 0.1 range -100.0 .. 500.0;
-- fixed-point with step 0.1; out-of-range assignments raise Constraint_Error

Constrained arrays & modular arithmetic

type Byte is mod 2**8;  -- wrap-around arithmetic modulo 256
type Packet is array (1 .. 128) of Byte;

Tasks & protected objects

protected Ring_Buffer is
  procedure Put (X : in Integer);
  entry Get  (X : out Integer);
private
  Buf : array (1 .. 16) of Integer := (others => 0);
  Head, Tail, Count : Integer := 0;
end Ring_Buffer;

protected body Ring_Buffer is
  procedure Put (X : in Integer) is
  begin
    while Count = 16 loop null; end loop;  -- simple backpressure (illustrative)
    Head := (Head mod 16) + 1;  Buf(Head) := X;  Count := Count + 1;
  end;

  entry Get (X : out Integer) when Count > 0 is
  begin
    Tail := (Tail mod 16) + 1;  X := Buf(Tail);  Count := Count - 1;
  end;
end Ring_Buffer;

Contracts

function Sqrt (X : Float) return Float
  with
    Pre  => X >= 0.0,
    Post => Sqrt'Result >= 0.0 and then
            abs (Sqrt'Result * Sqrt'Result - X) < 0.0001;

These aren’t just “nice to have” features; they encode intent into code, letting compilers and provers be partners instead of passive observers.

11) Tooling, compilers, and the developer experience

For teams used to contemporary developer experience, these tools bridge the gap between “classic” Ada and today’s pipelines.

12) Certification, standards, and why Ada saves money

Certification standards (e.g., DO-178C in avionics) don’t mandate a language—but they do mandate evidence. Evidence of absence of certain classes of defects. Evidence of traceability from requirement to implementation to test/proof. Evidence that changes didn’t break critical assumptions.

Ada reduces the cost of producing this evidence:

Certification is a multi-year, multi-million-dollar endeavor. Any language that efficiently supports evidence production changes the economics of safety.

13) Performance: safety vs. speed is a false binary

Ada is compiled, optimized, and close to the metal. Many run-time checks can be toggled (on in development, selectively off in production after proof or sufficient coverage). The fixed-point and modular arithmetic features are built for embedded performance. With representation clauses, you can specify memory layouts precisely. In practice, many Ada systems meet stringent timing constraints in avionics and rail—places where missed deadlines are failures, not “slower UX.”

The key is predictability: a small constant overhead that you can reason about often beats a theoretically faster model whose tail latencies become mission risks.

14) Interoperability: the real world is polyglot

It’s rare to find a green-field, single-language codebase in a complex system. Ada acknowledges that:

Ada doesn’t try to absorb the world. It tries to be the rock-solid part of it.

15) Case sketches (anonymized patterns)

These are not hypothetical acrobatics—they reflect how Ada/SPARK are typically wielded: clarity first, proofs where they pay the most, testing where proofs would be uneconomical.

16) Learning Ada in 2025: a practical path

  1. Install GNAT + Alire. That gives you the compiler and a package manager.
  2. Work through a small, concrete embedded-flavored project. For example, a telemetry ring buffer with backpressure, then evolve it into a tasking demo with a periodic sampler and a consumer.
  3. Add contracts. Start with Pre/Post and a few type invariants. Turn on run-time checks to see them fail fast when assumptions are violated.
  4. Try SPARK on a module. Port a small, critical piece to SPARK (absence of runtime errors proof). Observe how much the tool discharges automatically.
  5. Explore Ravenscar. If you’re curious about hard real-time, learn its restrictions and benefits; re-architect your prototype accordingly.
  6. Interoperate. Wrap a C library, or call Ada from C. Learn representation clauses and calling conventions.
  7. Measure. Add timing hooks, profile, and test worst-case. The point is not micro-benchmarks; it’s predictability.

The goal is to feel Ada’s design: the way types and contracts shift effort earlier, the calm that determinism brings to concurrency, the relief when a proof removes an entire testing stress category.

17) Common objections, answered briefly

18) Ada’s quiet lesson to software engineering

Ada teaches an unfashionable truth: discipline pays compounding dividends. Strong types shrink bug classes. Contracts align code and intent. Deterministic concurrency makes timing analysis tractable. Formal methods convert “we tested a lot” into “we proved it cannot happen.”

The discipline doesn’t eliminate creativity; it channels it. Instead of wrestling with undefined behavior, engineering energy goes into modeling the real world precisely: ranges that match sensors, contracts that match physics, schedules that match deadlines. The result is software that can be reasoned about—by humans, by compilers, and by provers.

19) Interesting corners you might have overlooked

Conclusion: The case for Ada in one paragraph

Ada is not a relic; it’s a living embodiment of an engineering philosophy: build software that can be trusted for decades, under constraints, in the presence of real-world failure modes. Its type system, contracts, concurrency model, and SPARK’s formal verification make it uniquely suited to safety-critical domains where evidence—not optimism—wins certifications. In an industry that often celebrates speed over certainty, Ada is the counterexample that keeps airplanes flying, trains stopping, and devices healing—quietly, relentlessly, and without drama.

Whether one writes web services or writes the code that keeps an aircraft level, Ada repays attention. The rumors of its obsolescence confuse popularity with importance. In the subset of software where bugs cost people their lives, Ada never left the front line.