https://www.iqiipi.com/the-quiet-colossus.html

Essay * Software & Ideas

The Quiet
Colossus

On Ada, the language that the Department of Defense built, the
industry ignored, and every modern language quietly became

There is a language that made generics a first-class, standardised
feature of a widely deployed systems language, formalised the
package, built concurrency into the specification rather than the
library, mandated the separation of interface from implementation,
and introduced range-constrained types, discriminated unions, and a
model of task communication that Go would arrive at, independently
and by a different route, thirty years later. Successive revisions
added protected objects, compile-time null exclusion, and
language-level contracts. It is a language that Rust spent a decade
converging toward from one direction while Python converged toward it
from another, and that C# has been approximating, feature by feature,
for the better part of two decades. It is a language that the
industry has consistently described as verbose, arcane, and
irrelevant. It is also, with a directness that embarrasses the usual
story of software progress, the language that anticipated -- with
unusual precision -- the safety features every modern language is now
trying to acquire.

Ada is not famous. It is not the subject of enthusiastic conference
talks or breathless blog posts. It does not have a charismatic
founder who gives keynotes about the philosophy of programming, and
it does not have a community that writes frameworks or publishes
packages with clever names. What it has is a formal standard that has
been revised four times since 1983; a presence in the software of
many major commercial aircraft and avionics systems; a set of design
decisions made under government contract in the late 1970s that the
rest of the industry has spent forty years independently
rediscovering; and a reputation, among the programmers who know it at
all, as the language that says no -- the language whose compiler
enforces legality, visibility, typing, and a degree of safety
checking that most languages leave to convention or tooling, that
makes the programmer name what they mean, that treats ambiguity as an
error rather than a feature. These qualities were, for a long time,
considered its weaknesses. They are, on examination, the precise
qualities that every language currently described as modern is
attempting to acquire.

* * *

To understand why Ada exists requires understanding the particular
crisis that produced it -- a crisis not of computer science but of
procurement, one that the United States Department of Defense
encountered in the early 1970s when it attempted to survey the
software that ran its weapons systems, logistics infrastructure, and
command-and-control apparatus. What the survey found was not a
software monoculture. It was the opposite: a proliferation of over
four hundred and fifty distinct programming languages and dialects in
active use across DoD systems, each one associated with a particular
contractor or a particular era of development, none interoperable
with any other, most unmaintainable by anyone except the original
authors, many of those authors no longer available.^1 The software
that guided missiles could not be maintained by the people who
maintained the software that navigated ships. The software that
scheduled logistics could not share code with the software that
processed communications. The languages had accumulated the way
technical debt accumulates: invisibly, incrementally, each individual
decision locally reasonable, the aggregate catastrophic.

The DoD's response was, for a government body, unusually
sophisticated. Rather than simply mandating an existing language --
COBOL, Fortran, and PL/1 were all considered and rejected -- it
undertook a requirements process that lasted five years and produced
a series of documents of increasing precision: Strawman, Woodenman,
Tinman, Ironman, and finally Steelman, each one refining and
tightening the specification of what a DoD programming language must
be. The Steelman document, issued in 1978, is a remarkable piece of
engineering requirements literature: it does not specify a language,
but describes the properties a language must have -- properties
derived from the actual failure modes of the DoD's existing software
estate. It requires a module system with explicit separation of
interface and implementation. It requires strong, static typing with
no implicit conversions between types. It requires built-in support
for concurrent tasks. It requires a consistent exception-handling
mechanism. It requires that the language be machine-independent. It
requires that programs be readable by people other than their
authors. It requires that the language make program verification
tractable. These were not aspirational preferences. They were
requirements derived from the observed consequences of programs that
lacked them.^2

In 1979, a competition among four finalists -- teams designated Green,
Red, Blue, and Yellow -- produced a winner: the Green design, by a
team led by Jean Ichbiah at CII Honeywell Bull in France. The winning
design was named Ada, after Augusta Ada King, Countess of Lovelace,
the nineteenth-century mathematician who wrote what is generally
considered the first algorithm intended for mechanical computation.
The choice of name was deliberate: the DoD wanted a name rather than
an acronym, wanted to honour a woman in a field that had few women
celebrated in it, and wanted to signal that the language was a
statement of intent rather than a committee compromise. Ichbiah took
the assignment seriously enough to accompany the standard with a
rationale document -- a full explanation of every design decision and
the reasoning behind it -- which is still, for anyone who reads it,
one of the most lucid accounts in existence of what programming
language design is actually for.

* * *

The centre of Ada's architecture is the package: a compilation unit
consisting of a specification and a body, physically separate, with a
relationship between them that the compiler enforces. The
specification is the contract -- it declares what the package
provides: types, subprograms, constants, whatever the package makes
available to the world. The body is the implementation -- it provides
the code that fulfills the contract. The specification is what client
code sees. The body is invisible to client code and can be compiled
independently, changed without recompilation of anything that depends
only on the specification, and replaced entirely without any client
knowing or caring. This separation is not a style recommendation. It
is not enforced by a linter. It is a structural property of the
language: client code that attempts to access anything not declared
in the specification will not compile, because the compiler will not
permit it to see the body.^3

This is the module system that every language that came after Ada has
been trying to build. Java's packages are not this: they are
namespacing mechanisms with access modifiers, but the implementation
is visible to reflection, to subclasses, and to code within the same
package that may not have been anticipated. Python's modules are not
this: they are files, with no formal separation between interface and
implementation, no compiler to enforce the boundary. JavaScript's
module system -- introduced in 2015, thirty-two years after Ada's --
provides import and export but no mechanism for a type to have a
specification whose representation is hidden from importers. C's
header files approximate the separation but without a compiler that
can verify consistency between the header and the implementation or
prevent the implementation's details from leaking through
preprocessor macros. Go's exported identifiers -- capitalised names
are visible, lowercase names are not -- achieve a related effect but
without the formal specification-body distinction. Rust's module
system with pub visibility rules is again an approximation. None of
these is quite Ada's package system, because none of them makes the
separation as structurally complete: in Ada, the implementation of a
private type is not merely inaccessible, it is syntactically absent
from the client's view of the world. It does not exist, as far as the
client is concerned. There is nothing to access, reflect on, or
circumvent.

Ada's package specification is not a convention. It is a contract
enforced by a compiler that refuses to let the client know the
implementation exists.

The private type mechanism, which flows naturally from the package
architecture, gives Ada something that took every other language
decades to approximate. A type declared private in an Ada package
specification is visible by name -- client code can declare variables
of that type, pass them to subprograms, return them from functions --
but its representation is completely opaque. The client does not know
whether the type is a record, an array, an integer, a pointer, or any
other thing. It cannot access fields, because it does not know there
are fields. It cannot copy the value in ways the designer did not
intend, because it does not know how the value is laid out. The
designer of the package decides what operations exist on the type,
declares them in the specification, and the rest of the world uses
only those operations. This is not access control in the sense of
Java's private keyword, which prevents direct access while leaving
the representation visible to inheritance, to reflection, and to the
compiler itself when it checks subclass compatibility. It is
representational invisibility: the type's structure literally does
not appear in the text that client code compiles against.

C# spent the better part of its existence providing access modifiers
and then slowly building toward genuine encapsulation through
mechanisms like record types, init-only properties, and sealed
classes. Java's evolution toward genuine data hiding has been
similar: records arrived in Java 16, in 2021, providing a class form
whose representation is fixed and whose accessors are generated --
thirty-eight years after Ada made representational hiding the default
for any type declared private. The journey of object-oriented
languages toward Ada's package system is the journey of people who
were told that access modifiers were encapsulation, discovering
gradually that they were not, and rebuilding from scratch what Ada
had provided from the beginning.

* * *

Ada's type system was, in 1983, unlike anything else in production
use, and remains, in its essentials, more expressive than most
languages that exist today. The distinction that organises it is
between a type and a subtype -- not in the object-oriented sense of a
type that extends another, but in the mathematical sense of a
constrained set. An Ada programmer who needs a type representing the
age of a person does not reach for int and add a comment. They write
type Age is range 0 .. 150, and the compiler generates, without
further instruction, a type whose values must lie in that range,
whose arithmetic operations are checked against that range at runtime
unless the programmer opts into unchecked operations explicitly, and
which is a distinct type from every other integer type in the
program, so that passing a calendar year where an age is expected is
a compile-time error rather than a runtime surprise or a silent wrong
answer.^4

This was not incremental. In the landscape of 1983, C had int and
short and long, distinguished by size and signedness but not by
meaning. Fortran had INTEGER and REAL. Pascal had ordinal subtypes
but not named distinct types with semantic constraints. Ada's range
types, enumeration types, and fixed-point types gave the programmer
the ability to encode meaning directly in the type system -- to make
the type be a machine-checked specification of what the value may be.
Rust's u8, i32, u64 are size-and-signedness distinctions that prevent
some errors; Ada's range types are semantic constraints that prevent
different, more domain-specific errors. Haskell's newtype wrapping
provides a closely related mechanism, reaching Ada's destination via
a different route. TypeScript's branded types -- a workaround pattern
involving phantom type parameters, widely used precisely because
TypeScript's structural type system otherwise collapses all integers
together -- exist to solve the problem that Ada named and solved in
1983.

Ada's discriminated record types are more significant still. A
discriminated record is a record type with a variant field -- a field
whose value determines what other fields exist. A shape might have a
discriminant selecting between circle and rectangle; a circle has a
radius field; a rectangle has width and height fields; the compiler
knows which fields exist for which discriminant value and will not
compile code that accesses a rectangle's radius. This is the
algebraic data type, the sum type, the tagged union -- the mechanism
that functional programmers have been advocating for decades as the
correct way to model data that can be one of several things. Haskell
has it as the core of its type system. Rust's enum with data fields
is precisely a discriminated union, implemented with the same
compiler guarantees Ada provided. Swift has associated value enums
for the same reason. Kotlin has sealed classes. TypeScript has
discriminated union types, added in version 2.0 in 2016. Ada had
discriminated record types in 1983, with compiler-enforced field
access checks and the ability to use them as discriminants of other
types, forming structures of arbitrary complexity. Every language
that has added sum types in the past twenty years has added, with its
own syntax, what Ada's designers put in the original standard.

Ada's discriminated record is the algebraic data type. Every language
that has added sum types in the past twenty years has independently
re-arrived at a 1983 design decision.
* * *

Ada's generic units are, of the language's many contributions,
perhaps the one whose influence is most direct and most consistently
unacknowledged. A generic in Ada is a parameterised package or
subprogram -- a template that can be instantiated with specific types
or values to produce a concrete package or subprogram. A generic sort
procedure takes a type parameter, an array type parameter, and a
comparison function parameter; it can be instantiated to sort
integers, or strings, or any type for which a comparison function can
be supplied. This is parametric polymorphism: the ability to write
code once and apply it to many types, with the compiler verifying
correctness for each instantiation rather than deferring the check to
runtime or relying on duck typing. Ada had this in 1983.

C++ had templates from approximately 1990. Java had no generics until
2004 -- twenty-one years after Ada -- and when Java's generics arrived
they were implemented through type erasure, which means the type
parameters exist at compile time but are removed before the program
runs, preventing the kind of runtime type specialisation that Ada's
generics make available. C# got generics in 2005 with a more complete
implementation that preserves type information at runtime -- closer to
Ada, but twenty-two years later. Go had no generics at all until
version 1.18 in 2022 -- thirty-nine years after Ada -- and their
absence was widely experienced as a significant limitation during
Go's first decade of use. Rust has generics with monomorphisation:
each instantiation of a generic type produces a concrete type at
compile time, the same approach Ada takes. The design space that
Rust's generics explore was charted in Ada's standard of 1983.^5

Ada's generic formal parameters are more expressive than most modern
generic systems. A generic unit in Ada can take as parameters not
just types but subprograms -- you can pass a function as a formal
parameter to a generic and have the compiler verify that it has the
right signature -- and packages, allowing a generic to be
parameterised by a whole module rather than just a type. This is
higher-kinded polymorphism by another route: the ability to abstract
over not just values but over type constructors and module
structures. Haskell's type classes reach a similar expressive power
by a different mechanism. Rust's trait system approaches it. C++
concepts, added in C++20 in 2020, allow generic type parameters to be
constrained by requirements on their operations -- which is what Ada's
generic formal type parameters have always specified. The forty-year
gap between Ada's feature and C++'s adoption of the same idea is not
unusual in this story.

* * *

Ada's concurrency model is where the gap between what Ada designed
and what the industry accepted becomes most consequential, because
the industry's failure to accept Ada's model is the direct cause of
the concurrency crisis that the industry spent the 2000s and 2010s
attempting to resolve. The crisis -- shared mutable state made
catastrophic by multicore processors, lock-based synchronisation
producing deadlocks and race conditions that testing could not
reliably detect -- was not unforeseeable. It was foreseen,
specifically, by the designers of Ada, who designed around it in 1983
and produced, in Ada 95, a concurrency model that subsequent
languages have been approximating ever since.

Ada tasks are language-level constructs: declared with task,
scheduled by the Ada runtime, communicating through either rendezvous
or protected objects. The rendezvous is a synchronised communication
point: a calling task names an entry it wishes to use, an accepting
task names the same entry in an accept statement, and neither can
proceed until both are ready. The communication happens at the
meeting; the tasks never share memory implicitly; the calling task
cannot reach into the accepting task and modify its state, because
the communication model provides no mechanism for doing so. This is
message passing -- not in the sense that a value is serialised and
sent over a socket, but in the sense that the design of the
communication prevents shared-state access by construction. Go's
channels are a direct instantiation of this idea with different
syntax and a slightly different semantics. The Go designers arrived
at channels by thinking carefully about concurrency safety; Ada's
designers arrived at rendezvous by the same route, thirty years
earlier.^6

Ada 95's protected objects address the cases where shared state is
genuinely required. A protected type wraps data and declares
operations on it: protected procedures, which have exclusive
read-write access; protected functions, which may be called
concurrently because they are read-only; and protected entries, which
are like procedures but include a barrier condition -- a boolean
expression that must be true for the operation to proceed, with the
calling task suspended automatically until the condition is
satisfied. The runtime enforces mutual exclusion for procedures and
entries without the programmer writing a lock. The barrier condition
for entries is re-evaluated whenever any operation completes,
providing a safe conditional wait without the manual condition
variable signalling that Java's concurrency model requires. Rust's
Mutex and RwLock types protect data in a related way -- wrapping state
in a type that enforces access discipline -- but through a library
rather than a language construct, and without the barrier condition
mechanism. Java's synchronized, wait, and notify are what programmers
reach for instead, and the combination is an invitation to subtle
errors: forgetting to synchronise, notifying the wrong condition,
holding a lock while calling foreign code. Ada's protected objects
make these errors structurally unavailable rather than merely
discouraged.

The SPARK subset of Ada extends the concurrency guarantees to formal
proof. SPARK excludes aliasing between task-accessible state,
constrains side effects in subprograms to those declared in the
subprogram's contract, and provides a static analysis toolchain that
can prove, mathematically rather than empirically, that a program has
no data races, no unhandled exceptions, no out-of-bounds array
accesses, and no violations of stated preconditions and
postconditions. Rust's borrow checker prevents a class of memory
safety errors at compile time, which is a related but narrower
guarantee: it prevents use-after-free, double-free, and certain kinds
of aliased mutation, but it does not formally prove the program's
logic correct. SPARK proves both the memory safety and the logic. The
space between Rust's compile-time rejection of unsafe programs and
SPARK's formal proof of correct programs is the space between
engineering discipline and mathematical verification -- and SPARK has
occupied the latter position, in production systems, since before
Rust existed as a project.^7

Go's channels and Ada's rendezvous are close relatives in the broader
CSP tradition. Rust's borrow checker prevents a subset of what SPARK
proves. The industry spent thirty years converging toward positions
Ada had staked out from the start.
* * *

Ada 2012 added contracts to the language: preconditions,
postconditions, and type invariants, expressible in Ada's own syntax
and checked by the compiler or by the runtime at the programmer's
direction. A subprogram's precondition is a boolean expression that
must hold when the subprogram is called; its postcondition is a
boolean expression that must hold when it returns; a type invariant
is a property that must hold for every value of a type whenever that
value is visible to outside code. These are not assertions in the
sense of runtime checks that may be disabled in production. They are
specifications: machine-readable statements of what a subprogram
requires and guarantees, which can be verified by the SPARK toolchain
without executing the program at all.^8

Design by contract -- the idea, named and systematised by Bertrand
Meyer in the Eiffel language in 1986 -- is the conceptual foundation
of this mechanism. Eiffel had it first; Ada 2012 formalised it in a
language with a large existing user base, a formal standard, and a
verification toolchain capable of using the contracts for static
proof rather than merely runtime checking. The idea's trajectory
through the wider industry has been slow. C++ has no standard
contract mechanism despite proposals dating to the early 2010s; C++20
deferred a contracts proposal that had been in preparation for years.
Java has never had contracts in the language; DbC in Java is done
through libraries, or through Javadoc conventions, or through JUnit
tests that approximate the postcondition check. Python's type hint
system, introduced in version 3.5 in 2015 and progressively extended
since, is a partial approach to contracts: it specifies types of
inputs and outputs but not behavioural properties. Rust's trait
bounds and type constraints are another partial approach. None of
these provides what Ada 2012 provides: a standard,
compiler-integrated notation for stating what a subprogram requires
and guarantees, checkable at runtime during development and provable
statically by a toolchain that ships with the language.

The direction of travel in every major language is toward contracts.
TypeScript's type system grows more expressive with each release,
adding conditional types, template literal types, and increasingly
fine-grained narrowing -- all of which are approximations of what a
contract-capable type system can express directly. Python's typing
module grows with each version, adding protocols, TypedDict,
ParamSpec, and Concatenate -- building, incrementally, toward the kind
of interface specification that Ada has had since 1983. C#'s nullable
reference types, added in version 8.0 in 2019, impose a constraint
that Ada's access type design imposed from the beginning: references
must be explicitly declared nullable to permit the null value, and
the compiler enforces the distinction. The nullable reference crisis
-- null as the billion-dollar mistake, Tony Hoare's self-described
worst design error -- is a crisis that Ada mitigated but did not
solve. Ada's access types are initialised to null by default, and
dereferencing a null access value raises Constraint_Error at runtime
-- a defined behaviour, unlike C's undefined behaviour on null
dereference, but a runtime check rather than a compile-time
guarantee. Ada 2005 introduced not null access type annotations,
allowing the programmer to declare that a particular access value may
never be null and having the compiler enforce the restriction
statically. This is genuine compile-time null safety, but it is
opt-in, added twenty-two years after the original standard, and not
the default. C#'s nullable reference types, added in version 8.0 in
2019, take the same opt-in approach from the opposite direction:
references are assumed non-null unless explicitly annotated as
nullable. Both languages arrived at the same architectural insight --
that nullability should be visible in the type -- but neither made it
the default from the start, and neither can claim to have eliminated
the problem that Hoare identified. What Ada provided from the
beginning was the safer failure mode: a raised exception rather than
corrupted memory.

* * *

The exception handling model that Ada introduced in 1983 was the
first production realisation of structured exception handling -- the
idea that exceptions are not simply jumps to an error handler but
events that are raised, propagated through a defined call stack, and
handled in an exception handler that is syntactically associated with
the block or subprogram that established it. Ada's model requires
that exceptions be declared before use, that handlers be associated
with specific scopes, and that the propagation rules be defined
precisely. C++ adopted structured exception handling in 1990, seven
years after Ada. Java went further than Ada in one significant
respect: Java's checked exceptions require that certain exception
types be either caught or declared in the method's throws clause,
making the caller's responsibility for handling failure part of the
function's compiled interface. Ada has no equivalent mechanism -- Ada
exceptions propagate freely through the call stack, and a
subprogram's specification says nothing about which exceptions it may
raise. Java's checked exceptions drew less from Ada than from CLU's
signalling mechanism and Modula-3's exception declarations, and the
experiment was contentious from the start: checked exceptions are
widely considered one of Java's design missteps, Scala and Kotlin
removed them entirely, and the industry has never settled the
question of whether the compiler should enforce exception awareness
at the call site.^9

Rust makes the related choice of removing exceptions entirely: errors
are values, returned from functions in a Result type, and the
question of whether a function can fail is expressed in its return
type rather than in a separate exception mechanism. This is a
different resolution of the same underlying problem -- that callers
must know whether a called function can fail and in what ways -- and
it reaches a conclusion that Ada's own exception model does not
reach: in Ada, as in C++ and Python, exceptions are a hidden channel,
propagating through the call stack without appearing in the
subprogram's specification, and a caller can forget about them
entirely until they arrive. Rust's error-as-value approach and Java's
checked exceptions are two different attempts to close that channel.
Ada's contribution was not to close it but to structure it -- to
replace the raw jump of setjmp/longjmp and the ambiguity of signal
handlers with a mechanism whose propagation rules were defined, whose
handlers were scoped, and whose behaviour was predictable. That
structuring was the foundation on which every subsequent exception
system was built, even the systems that went further than Ada was
willing to go.

* * *

Ada's annexes -- the optional extensions to the core language, defined
in the standard, requiring separate compiler certification --
represent a design decision that no other language has replicated and
that the industry might have benefited from considering. The annexes
define features for specific domains: real-time systems, distributed
systems, information systems, numerics, safety and security,
high-integrity systems. A compiler that implements Annex C for
systems programming must implement certain predefined attributes and
representation clauses. A compiler that implements Annex D for
real-time systems must implement task priorities, scheduling
policies, and time constraints in ways the standard specifies. The
certification that a compiler conforms to an annex is independently
verifiable. The user of a compiler knows precisely what it supports
and does not support, because the support is a documented, testable
claim against a formal standard rather than an emergent property of
whatever the compiler's authors chose to implement.^10

No other mainstream language has this model. JavaScript's feature
support is tracked through compatibility tables because the standard
and the implementation are separate worlds with no formal coupling.
Python's standard library coverage varies between implementations --
CPython, PyPy, and MicroPython are different things that call
themselves Python. Rust's feature set is formally stable or unstable,
but the boundary between the two moves over time and the notion of
certifiable compliance does not exist. C++ compilers compete on which
features of the latest standard they have implemented rather than on
certified compliance with any defined subset. Ada's annex model is
the idea that a standard should be a contract -- testable,
certifiable, useful precisely because it specifies not just what is
permitted but what is required. The DO-178C standard for airborne
software certification, which governs the software in every certified
civil aircraft, requires documentation and process evidence that a
formally standardised language with certifiable compiler conformance
makes considerably easier to produce. Ada's standard, with its annex
structure and conformance testing scheme, fits DO-178C's requirements
with unusual directness. C and C++ can meet the same certification
requirements -- and do, routinely -- but through additional process
documentation and tooling rather than through a standard that was
designed with certification in mind. Ada's standardisation and
tooling make it unusually well suited to certification-heavy domains;
they do not make it the only language that can operate in them.

* * *

The question of why Ada's influence is so consistently unacknowledged
has several answers, none of them fully satisfying. The most
straightforward is institutional: Ada was a government language,
procured through a process that Silicon Valley was not watching and
would not have respected if it had been. The designers of C++, Java,
and Python were not reading the Steelman document. They were solving
the problems in front of them -- making C safer, making software
objects work, making scripting simple -- and their solutions converged
on Ada's solutions not because they were following Ada but because
the problems were the same problems and the good solutions are the
good solutions.

A second answer is aesthetic. Ada's syntax is verbose in a way that
programmers with a background in C find unpleasant. if X then Y; end
if; instead of if (x) { y; }. procedure Sort (A : in out Array_Type)
instead of void sort(int* a). The verbosity was deliberate -- Ichbiah
wanted programs to be readable by people other than their authors,
and readability over time favours explicitness -- but it was
experienced as bureaucratic and un-hacker-like, and the programming
culture that formed in the 1980s and 1990s was organised around the
proposition that conciseness was sophistication. Ada was the language
of procurement officers. C was the language of people who understood
machines. The cultural verdict was delivered early and never
substantially revisited.

A third answer is that Ada's deployment domain meant that Ada's
successes were invisible. A software project that compiles without
error, runs without race conditions, and has been formally verified
to satisfy its specification does not generate incident reports or
post-mortems or conference talks about what went wrong. Ada's
successes -- the aircraft that have not crashed, the railway
signalling systems that have not failed, the missile guidance
software that has not misguided -- are invisible precisely because
they are successes. The languages that failed visibly, in buffer
overflows and null pointer exceptions and data races and security
vulnerabilities, generated the discourse. Ada generated reliable
software, and reliable software does not generate discourse.

Ada's successes are invisible because they are successes. The
languages that failed visibly generated the discourse. Reliable
software does not generate conference talks.
* * *

The trajectory of modern language design is, traced carefully, a
trajectory toward positions Ada occupied early. The type system
features that Rust, Haskell, TypeScript, and Swift are celebrated for
-- sum types, parametric polymorphism, constraint-based generics,
affine types and ownership -- each solve a problem that Ada identified
in 1983 and that the mainstream languages of the subsequent twenty
years declined to solve. The module systems that Go, Rust, and Swift
have been praised for -- explicit interfaces, separation of
specification from implementation, visibility control that the
compiler enforces rather than merely recommends -- are partial
implementations of what Ada's package system provided from the
beginning. The concurrency models that Go's channels and Rust's
ownership have been credited with inventing belong to the same CSP
and message-passing lineage as Ada's rendezvous and protected object
model, which provided production-grade answers to the same problems
in 1983 and 1995. The contract systems that C#'s nullable references,
TypeScript's type narrowing, and Python's gradual typing are
approximating, from different angles, are what Ada 2012 added to a
language that has been in continuous use since before most of its
practitioners were born.

This is not a claim that every modern language copied Ada, or that
Ada's designers deserve credit that has been withheld from them. Most
of the convergence is genuinely independent: the designers of Rust
did not derive the borrow checker from Ada's access type rules; the
designers of Go did not derive channels from Ada's rendezvous; the
designers of TypeScript did not derive discriminated unions from
Ada's variant records. The convergence is real but it is convergence
toward correct solutions to real problems, not plagiarism. Ada's
designers identified the problems first, and identified them with
unusual clarity, because they were designing for a context in which
the problems had already killed people and would kill more if the
solutions were wrong.

What Ada demonstrates is not that it should be more widely used --
though the argument for its use in any domain where software
reliability matters is stronger than the industry credit it receives
-- but that the problems modern language design is solving are old
problems, and that the solutions modern languages are discovering are
old solutions. The idea that null references require explicit
annotation, that concurrency requires language-level enforcement
rather than library-level convention, that interface and
implementation should be structurally separated, that type systems
should encode domain constraints rather than merely machine
representations, that generic code should be verifiable at
instantiation time -- these are not insights of the 2010s or the
2020s. They are insights of the 1970s and 1980s, formulated in
response to software failures whose consequences were concrete enough
that the people responsible for preventing them were willing to pay
for a language competition that lasted five years.

The industry has spent forty years building languages whose best
features converge, independently, on positions Ada staked out decades
earlier. It has spent the same forty years describing Ada as
irrelevant. The first observation and the second are in tension in a
way that the industry has not yet fully acknowledged, and that Ada --
deployed in aircraft overhead, in rail signals alongside the tracks,
in the guidance systems of spacecraft currently in transit between
planets -- has not needed to acknowledge, being too busy running
correctly to concern itself with the question of whether it is
appreciated.

1The DoD software crisis is documented in a series of internal
studies from the early 1970s, summarised in the 1974 report
Requirements for High Order Computer Programming Languages, which
identified 450 languages and dialects in use across DoD systems and
estimated that software costs were growing unsustainably. The figure
of 450 languages is cited in multiple histories of the Ada
development process, including the account in Jean Sammet and Fred
Neighbors, "The ADA Programming Language," Communications of the ACM,
1986. The specific cost projections that motivated the competition
are detailed in Fisher, David A., "A Common Programming Language for
the Department of Defense," 1976.

2The Steelman document -- formally "Requirements for High Order
Computer Programming Languages (Steelman)," June 1978 -- is the final
in a series of requirements documents whose earlier versions were
named Strawman (1974), Woodenman (1975), Tinman (1976), and Ironman
(1977). The documents are available from public archives and repay
reading: the evolution from Strawman to Steelman is a record of
requirements being refined by experience, and Steelman's final form
is notably precise about what it requires and why. The four competing
designs submitted in 1979 were evaluated against Steelman's
requirements by independent teams. All four passed the first
evaluation; Green and Red advanced to the final evaluation; Green was
selected. Jean Sammet chaired the High Order Language Working Group
that managed the competition.

3Ada's package structure is specified in chapter 7 of the Ada
Reference Manual (ARM). The separation of specification and body is
enforced at compilation: a package body must be consistent with its
specification, and client code compiled against the specification
cannot see the body. The private part of a package specification --
between the private keyword and the end of the specification -- is
visible to the compiler when compiling client code (so that the
compiler can allocate storage for private type objects) but not
semantically available: client code cannot reference anything defined
only in the private part. The Ada Rationale (Ichbiah et al., 1979)
explains this design as an explicit rejection of the public-field
patterns that were common in the systems languages of the era.

4Ada's type system, with its distinction between types and subtypes
and its support for range constraints, enumeration types, fixed-point
types, and modular types, is described in chapters 3 through 5 of the
ARM. The design principle -- that a type is a set of values and a set
of operations, and that different semantic domains require different
types even when their representation is identical -- is stated
explicitly in the Ada Rationale and attributed partly to the
influence of Barbara Liskov's CLU language and partly to the DoD's
operational requirement that programs mixing units (feet and meters,
pounds and kilograms) be detectable at compile time. The Ariane 5
rocket disaster of 1996, in which a 64-bit floating-point number was
converted to a 16-bit integer without range checking, destroying the
rocket 37 seconds after launch, occurred in Ada code that used
unchecked conversion to bypass Ada's type system. The disaster is
sometimes cited as a failure of Ada; it is more accurately a
demonstration of what happens when Ada's type checking is explicitly
circumvented.

5Ada's generic units are defined in chapter 12 of the ARM. Generic
formal parameters may be types (with various degrees of constraint),
subprograms, objects, or packages. The ability to pass packages as
generic parameters -- a form of higher-kinded polymorphism -- was
present in Ada 83 and has been elaborated in subsequent revisions.
Java's decision to implement generics through type erasure --
retaining type parameters at the source level but removing them in
compiled bytecode -- was driven by backwards compatibility concerns
and produced a generic system that cannot express operations
requiring runtime type information, cannot use primitive types as
type parameters, and generates compiler warnings (unchecked cast)
when interacting with legacy pre-generic code. C#'s reified generics
-- which preserve type information at runtime -- avoid these
limitations; Microsoft's designers were explicit that they had
studied Java's approach and chosen a different architecture. Both
approaches are less expressive than Ada's generic formal parameters,
which can be constrained to types that support specific operations,
checked at instantiation time, without the type erasure problem and
without the nominal inheritance required by Java's bounded wildcards.

6Ada's task rendezvous model is described in chapter 9 of the ARM.
The rendezvous design was influenced by C.A.R. Hoare's Communicating
Sequential Processes (CSP) formalism, published in 1978, which
provided a mathematical model of task communication through
synchronised events. Go's channels are also derived from CSP, with
the explicit acknowledgement of Rob Pike, who worked with Hoare's
ideas through his development of the Newsqueak and Limbo languages
before contributing them to Go. The line of descent from Hoare's CSP
through Ada's rendezvous and through Pike's channel model is a single
conceptual lineage, which makes the common framing of Go's channels
as a new idea a historical compression. Ada's protected objects,
added in Ada 95, were designed by Tucker Taft and others to address
the cases where shared state is required -- cases that the pure
rendezvous model handles awkwardly -- and drew on earlier work on
monitors and concurrent object models.

7SPARK Ada was originally developed by Program Validation Limited
(PVL) in the UK and is currently maintained by AdaCore, with the
primary static analysis tool being GNATprove. The SPARK language
definition is maintained separately from the Ada standard and
specifies a subset of Ada from which aliasing, unconstrained side
effects, and certain forms of dynamic dispatch are excluded.
GNATprove uses abstract interpretation and SMT (satisfiability modulo
theories) solvers to prove, without executing the program, that
subprograms satisfy their contracts, that array accesses are within
bounds, that integer operations do not overflow, and that tasks do
not race on shared state. The Airbus A380's primary flight control
system, the SHOLIS helicopter system, and the UK's MULTOS smart card
operating system are among systems that have been formally verified
in SPARK. Rust's formal verification toolsets -- Kani, Creusot, and
others -- are research and production tools that apply similar
SMT-based verification to Rust programs; they are newer, less mature,
and cover a smaller fraction of Rust's feature set than GNATprove
covers of SPARK.

8Ada 2012's contract model is specified in chapter 6.1 (preconditions
and postconditions) and 7.3.2 (type invariants) of the ARM.
Preconditions and postconditions are boolean expressions written in
Ada itself, evaluated on subprogram entry and exit respectively when
assertion checking is enabled. SPARK's toolchain uses the same
expressions as formal specifications for proof. Bertrand Meyer's
Eiffel language introduced the design-by-contract terminology and the
concept of invariants, preconditions, and postconditions in the
mid-1980s; Ada 2012's contract model is substantially aligned with
Eiffel's, though the integration with SPARK's proof system extends
the contracts beyond what Eiffel's runtime checking provides. C++20's
contracts proposal, which would have added preconditions and
postconditions to C++ with similar syntax, was withdrawn from the
C++20 standard after committee disagreement about semantics; as of
2024 a revised proposal is under development for a future standard.
The forty-year gap between Ada's precursors and C++'s adoption of
contracts is, in the history of language features, almost but not
quite the longest.

9Ada's exception model is defined in chapter 11 of the ARM. The
requirement that exceptions be declared and that their propagation be
through a structured call stack -- rather than through setjmp/longjmp
or signal handlers -- was part of the original Ada 83 design. The
Steelman document explicitly required "a uniform mechanism for
handling run-time errors and other exceptional situations." Ada's
exception model does not, however, include any mechanism for
declaring which exceptions a subprogram may raise: exceptions
propagate freely, and a caller has no compiler-enforced obligation to
handle or declare them. Java's checked exceptions -- which require
that certain exception types in a declared throws clause be either
caught or re-declared by callers -- went beyond Ada's approach,
drawing more directly from the exception mechanisms of CLU and
Modula-3. The checked exception model was controversial within Sun
from the start, and the subsequent history -- checked exceptions
widely considered a design mistake, RuntimeException and Error used
to circumvent the checking requirement, Scala and Kotlin removing
checked exceptions while keeping Java compatibility -- is a history of
the industry testing and largely rejecting a position that Ada's
designers did not take.

10Ada's normative annexes are defined at the end of the ARM: Annex C
(Systems Programming), Annex D (Real-Time Systems), Annex E
(Distributed Systems), Annex F (Information Systems), Annex G
(Numerics), and Annex H (High Integrity Systems). A compiler may
claim conformance to any subset of the annexes, with each conformance
claim subject to independent validation testing. The Ada Conformity
Assessment Authority (ACAA) administers the Ada Conformity Assessment
Test Suite (ACATS), a suite of tests that any conforming Ada
implementation must pass. The DO-178C standard for airborne software,
which governs software in civil aircraft certified by the FAA, EASA,
and equivalent authorities, requires documentation and process
evidence that higher certification levels (Design Assurance Level A
and B) make particularly demanding. Ada's formal standard, with its
annex structure and conformance testing scheme, provides evidence of
language-level guarantees in a form DO-178C can directly reference. C
and C++ are also widely used in DO-178C-certified software, with
equivalent certification achieved through additional process
documentation and qualified tooling. Ada's advantage in this context
is not exclusivity but fit: the language standard was designed, in
part, with the needs of certifiers in mind.

ERRATA

Exception handling and Java's checked exceptions. The original
version of this essay stated that Java's checked exceptions were "a
direct borrowing of Ada's idea that callers should know what
exceptions a subprogram may raise," and that Ada had exception
specifications "in its subprogram specifications as a standard
feature from the beginning." Both claims were wrong. Ada's exception
model requires that exceptions be declared as named objects and that
handlers be associated with specific scopes, but it does not require
-- and has never required -- that subprograms declare which exceptions
they may raise. Ada has no equivalent of Java's throws clause.
Exceptions in Ada propagate freely through the call stack; a caller
has no compiler-enforced obligation to handle or acknowledge them.
Java's checked exception mechanism went beyond what Ada provided, and
its intellectual lineage runs more directly through CLU's signalling
mechanism and Modula-3's exception declarations than through Ada. The
corrected text reflects Ada's actual contribution -- the structuring
of exception propagation into a defined, scoped, predictable
mechanism -- without overclaiming that Ada required callers to know
what a subprogram might raise. The accompanying footnote (9) and the
paragraph on Rust's error-handling model have been revised
accordingly.

Access types and null safety. The original version stated that the
nullable reference crisis was "a crisis that Ada did not have,
because Ada access types are initialised to null by default and the
compiler requires explicit null exclusion or null checking before
use," and that "C# arrived at enforced null safety thirty-six years
after Ada." This materially misrepresented Ada's null-handling
semantics. Ada access types do default to null, but dereferencing a
null access value is not a compile-time error -- it raises
Constraint_Error at runtime, which is a defined and recoverable
behaviour (unlike C's undefined behaviour on null dereference) but is
not compile-time null safety. The not null access type annotation,
which does provide compile-time null exclusion, was introduced in Ada
2005, twenty-two years after the original standard, and is opt-in
rather than the default. The corrected text describes what Ada
actually provides -- a safer runtime failure mode from the beginning,
and genuine but opt-in compile-time null exclusion from 2005 --
without the false claim that Ada solved the null problem from the
start.

Epigraphs. Three epigraph quotations attributed to Jean Ichbiah,
Bjarne Stroustrup, and Tucker Taft appeared in the original version.
None could be traced to a reliable primary or secondary source. They
have been removed.

"Invented the generic." The opening paragraph originally described
Ada as the language that "invented the generic." Parameterised
abstractions existed before Ada, notably in CLU (Liskov et al.,
1977). Ada made generics a first-class, standardised feature of a
widely deployed systems language, which is a different and more
defensible claim. The wording has been revised accordingly, and the
opening paragraph's compressed timeline -- which implied that all of
the essay's headline features shipped in 1983 -- has been expanded to
acknowledge that protected objects arrived in Ada 95, not null in Ada
2005, and contracts in Ada 2012.

"Go's channels are Ada's rendezvous with different syntax." A pull
quote and the trajectory paragraph both characterised Go's channels
as a re-implementation of Ada's rendezvous. The more accurate claim
is that both belong to the broader CSP/message-passing tradition
descending from Hoare's 1978 formalism. Go's own lineage runs
explicitly through Newsqueak and Limbo; the family resemblance to Ada
is real, but the direct-equivalence framing was too strong. The
corrected text describes them as close relatives in a shared lineage.

Aviation and DO-178C. The original text claimed Ada had "a presence
in the software of every commercial aircraft currently in service"
and that DO-178C effectively treats Ada's formal standard as a
prerequisite, implying other languages cannot be used in certified
airborne software. Neither claim is supported by the available
evidence. Ada is used in many major commercial aircraft and avionics
systems, but "every commercial aircraft" is unverifiable and almost
certainly false. DO-178C certification is routinely achieved with C
and C++ through additional process documentation and qualified
tooling, and Rust tooling for certification contexts is under active
development. The corrected text describes Ada's standardisation and
tooling as unusually well suited to certification-heavy domains
without claiming exclusivity. Footnote 10 has been revised
accordingly.

Footnote 3: "friend-class" anachronism. The original footnote
attributed to the Ada Rationale an explicit rejection of
"friend-class and public-field patterns that C was making common."
The friend keyword is a C++ feature (Stroustrup, 1985), not a C
feature; it did not exist in the language landscape of 1979. The
unsourced Ichbiah quotation ("the private part as a structural
firewall") has also been removed. The footnote now references the Ada
Rationale's rejection of public-field patterns in the systems
languages of the era without the anachronistic C++ attribution.

"The language that refuses to compile programs it cannot verify." The
original second paragraph described Ada as "the language that refuses
to compile programs it cannot verify." This overstates what the Ada
compiler enforces. An Ada compiler checks legality, visibility,
typing, accessibility, and many safety-related constraints, but full
formal verification -- proof of absence of runtime errors, data races,
and contract violations -- is the province of SPARK and GNATprove, not
of ordinary Ada compilation. The corrected text describes the
compiler's actual enforcement without conflating it with formal
proof.