The Quiet
Colossus

On Ada, the language that the Department of Defense built, the industry overlooked, and modern software keeps rediscovering

There is a language that took generics — an idea explored in CLU and present in research systems of the 1970s — and made them a first-class, standardised feature of a widely deployed systems language. It took the subrange types of Pascal and the variant records of Pascal and CLU and deepened them into a type system of unusual rigour. It built concurrency into the language specification rather than the library. It mandated the separation of interface from implementation. It drew, among other sources, on C. A. R. Hoare's formal work on communicating processes and produced a model of task communication that belongs to the same broad lineage as the channels Go would popularise decades later by a different route. Ada was first standardised as MIL-STD-1815 in 1980; the canonical Ada 83 standard followed in 1983. Later revisions added protected objects in 1995, not null exclusion for access types in 2005, contract features in 2012, and further refinements in 2022. It is a language the industry has spent decades calling verbose, bureaucratic, and obsolete. It is also, with a directness that embarrasses the usual story of software progress, a language that anticipated — with unusual precision — many of the safety features modern languages are now independently acquiring.

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. It has a formal standard that has been revised four times since 1983. It has a presence in the software of many major commercial aircraft and avionics systems. It has a set of design decisions, made under government contract in the late 1970s, that later languages have, in whole or in part, independently rediscovered. And it has 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, many of the qualities that languages now described as modern have been working 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 surveyed 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, most tied to a particular contractor or a particular era of development, few interoperable, many unmaintainable by anyone except the original authors.¹ 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 roughly 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 modularity with explicit separation of interface and implementation. It requires strong, static typing. 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.²

These are easy requirements to applaud now, because the industry has since made them sound like common sense. In the 1970s they were less obvious than they now appear. They had to be extracted from costly experience.

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, and wanted to honour a woman in a field that had few women celebrated in it. Ichbiah accompanied the standard with a rationale document — an extensive explanation of the major design decisions and the reasoning behind them — which remains, for anyone who reads it, one of the most lucid accounts in existence of what programming language design is actually for.

Ada did not arise in isolation. Its designers were fluent in the research languages of the decade: Barbara Liskov's CLU, which had pioneered parameterised abstractions, structured exception handling, and type-safe variant forms; Niklaus Wirth's Pascal, which had introduced subrange types and variant records; Hoare's formal models of concurrent communication; and the hard lessons of Fortran, COBOL, and the systems languages that had produced the crisis Steelman was written to resolve. What Ichbiah's team did was not to invent from nothing. It was to synthesise — to take the best ideas available in the research literature and forge them, for the first time, into a single standardised language intended for large-scale systems work, backed by a formal standard, accompanied by a rationale, and designed from the start with verification, safety, and long-term maintenance as first-order concerns. The individual ingredients existed. The combination did not.

The centre of Ada's architecture is the package: a compilation unit consisting of a specification and, where needed, 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 so long as the specification and its behavioural assumptions remain compatible. 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.³

This matters not because no other language has a module system, but because Ada made a particularly strong and explicit version of one a built-in structural feature — and made it early. 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 imperfectly: the preprocessor can leak implementation details, and consistency between header and source is only partially enforced. 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 closer still. Ada's package design is not the only good answer to modularity. It is, however, an early and unusually rigorous one, and it is striking how many later answers have moved in its direction.

The private type mechanism, which flows naturally from the package architecture, gives Ada a form of encapsulation stronger than the ordinary use of access modifiers in many object-oriented languages. 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. 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. Predefined operations — assignment, equality — still exist unless the designer restricts them further, but the representation itself is invisible. 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.⁴

The point is not that every later language has been trying, unsuccessfully, to recreate Ada's package system. It is that Ada treated abstraction boundaries as a first-order semantic concern rather than as a matter of etiquette — and that the distance between "access modifiers" and genuine representational hiding turns out to be larger than the object-oriented mainstream long assumed. C#'s gradual construction of genuine encapsulation through record types, init-only properties, and sealed classes; Java's late arrival of records in Java 16, in 2021 — these are not derivatives of Ada. They are independent discoveries of the same insight Ada's designers built in from the beginning. The journey is the same; the routes are different.

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.⁵

The concept of constraining a type to a range was not new. Pascal had subrange types a decade earlier. What Ada added was the combination: range constraints fused with strong type distinction, so that two types with identical ranges but different meanings could not be confused; enumeration types that were named values rather than disguised integers; fixed-point types that encoded numeric precision directly in the type system. The language encourages the programmer not merely to say what size a value is, but what kind of thing it is. That remains a live issue. Haskell's newtype wrapping provides a closely related mechanism, reaching the same destination via a different route. Rust's penchant for newtype wrappers arises from the same recognition. 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. When semantically different values collapse into a single undifferentiated numeric or structural type, bugs become easy to write and hard to see. The recognition is perennial; the solutions recur.

Ada's discriminated record types belong to the same story. 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 closely analogous to what is now called 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. Pascal had variant records earlier, and CLU had type-safe variant forms. Ada did not invent the whole family. It did deepen the mechanism with compiler-enforced field access checks and provide an early, standardised, industrial form of it. Haskell, Rust, Swift, Kotlin, and TypeScript would later make sum-like modelling central to their own designs — each arriving independently, each solving the same durable problem.

Ada's generics are perhaps the cleanest case in which a feature long treated as modern turns out to have been present, in mature form, much earlier than the mainstream story usually admits. 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. CLU had parameterised abstractions in 1977. Ada took the idea and made it standard in 1983, in a language intended for production systems of enormous scale.

The chronological comparison is instructive, though it requires care. 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 reified generics that preserve type information at runtime. 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, architecturally closer to Ada's world than to Java's. Ada's generic system is not simply a primitive version of Rust's, nor is Rust a delayed Ada. The languages solve overlapping problems with different surrounding type systems and different design goals. What one can say, defensibly, is that Ada treated generic programming as a serious, standardised capability decades before many mainstream languages did.⁶

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, in effect, a form of abstraction over type constructors and module structures — the kind of expressiveness that Haskell's type classes reach by a different mechanism and that Rust's trait system approaches. 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 family resemblance is real, but it is not identity. Later languages reached related expressive territory by other means, often without knowing Ada had been there.

Ada's concurrency model is one of the places where the difference between its design ambitions and the industry's later habits becomes particularly revealing. Ada has language-level tasks. It has rendezvous: synchronised entry calls in which one task calls an entry and another task accepts it, with the communication occurring at a defined meeting point. It later acquired protected objects, which provide controlled shared-state access with enforced mutual exclusion and guarded entry conditions. Ada did not somehow solve all concurrent programming in 1983. But it took concurrency seriously as a language-design problem at a time when many popular languages did not — and the concurrency crisis of the 2000s and 2010s, in which shared mutable state made catastrophic by multicore processors produced deadlocks and race conditions that testing could not reliably detect, was not unforeseeable. It was, in part, a consequence of the industry's preference for concurrency approaches less disciplined than the one Ada had offered.

Ada tasks are language-level constructs: declared with task, scheduled by the Ada runtime, communicating through rendezvous, protected objects, and other mechanisms the language provides. 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 design provides no mechanism for one task to reach into another and modify its state. Go's channels and Ada's rendezvous are close relatives in the broader tradition descending from Hoare's 1978 formalism of Communicating Sequential Processes. Go's own lineage runs explicitly through Newsqueak and Limbo, languages Rob Pike developed before contributing the channel model to Go. The family resemblance to Ada is real, but neither is a copy of the other: both are independent descendants of the same conceptual ancestor, and both arrived at production-grade answers to the same problem by different routes.⁷

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 restricts aliasing between task-accessible state and constrains side effects in subprograms to those declared in the subprogram's contract. Its primary analysis tool, GNATprove, uses abstract interpretation and SMT solvers to prove — mathematically rather than empirically — that a program satisfies its contracts, that array accesses are within bounds, that integer operations do not overflow, and that tasks do not race on shared state. 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 can prove absence of runtime errors and verify user-stated functional properties when the necessary contracts and annotations are present. The comparison is not a contest in which one language must be declared the winner. It is a reminder that "compile-time safety" names several different tiers of ambition, and that Ada's ecosystem has long contained tools operating at a particularly demanding tier — in production safety-critical systems, since before Rust existed as a project.⁸

Ada 2012 added contracts to the language: preconditions, postconditions, and type invariants, expressible in Ada's own syntax, checked at runtime when assertion checking is enabled, and usable as proof obligations in SPARK. 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.⁹

Design by contract — the idea, named and systematised by Bertrand Meyer in the Eiffel language in 1986 — is the conceptual foundation of this mechanism. Ada did not invent the terminology or the foundational idea. Eiffel had it first. What Ada 2012 did was standardise contract notation in a mature language with an existing user base, a formal standard, and a verification toolchain capable of doing something more with those contracts than merely testing them at runtime. The industry's progress toward such features has been uneven. C++ deferred a contracts proposal from the C++20 standard after committee disagreement about semantics; a revised proposal (P2900) was finally adopted in C++26, shipped in 2026 — forty-three years after Ada's original standard and fourteen years after Ada 2012's contracts. 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 lesson is not that all of these languages are secretly trying to become Ada. It is that the desire to make expectations explicit — what a function requires, what it promises, what a value may be — is perennial, and Ada incorporated one unusually direct version of that desire into its standard language model. The nullable reference crisis — null as the billion-dollar mistake, Tony Hoare's self-described worst design error — illustrates the same pattern. Ada was better positioned than C from the beginning: dereferencing a null access value raises Constraint_Error at runtime, a defined and recoverable behaviour, unlike C's undefined behaviour on null dereference. But Ada did not begin with full compile-time null safety. Access values default to null; that is part of the original design. 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. C#'s nullable reference types later approached the same insight from a different default. 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. What Ada provided from the beginning was the safer failure mode: a raised exception rather than corrupted memory.

Ada's exception model, present in the 1983 standard, was among the earliest production realisations 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. CLU had explored structured exception handling earlier, and Ada's designers were aware of that work. What Ada did was bring the mechanism into a standardised systems language at industrial scale, requiring 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 around 1990, roughly 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 exception design 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.¹⁰

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. Ada's contribution was not to close that channel 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 — building on CLU's earlier work and scaling it to a language designed for systems of enormous complexity — 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 the industry might have benefited from considering more widely. The annexes define features for specific domains: systems programming, real-time systems, distributed systems, information systems, numerics, high-integrity systems. A compiler that implements an annex for systems programming must implement certain predefined attributes and representation clauses. A compiler that implements the real-time annex 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 through the Ada Conformity Assessment Test Suite. 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.¹¹

That model has never become fashionable in mainstream language culture, which tends to accept much looser relationships between standards, implementations, and platform behaviour. 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. 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. In certification-heavy domains that difference matters. The DO-178C standard for airborne software certification requires documentation and process evidence that a formally standardised language with certifiable compiler conformance makes considerably easier to produce. C and C++ can meet the same certification requirements — and do, routinely — but through additional process documentation and tooling. Ada's advantage in this context is not exclusivity but fit: the language standard was designed, in part, with the needs of formal certification in mind.

The question of why Ada's influence is so consistently underdescribed has several answers, none of them fully satisfying. The most straightforward is institutional: Ada was a government language, procured through a process that the commercial software industry was not watching closely. 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 the Steelman document explicitly required it — 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.

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 early, 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. And they did not work in a vacuum: they read CLU, they read Pascal, they read Hoare. They were, themselves, beneficiaries of a lineage. What they did was take that lineage seriously enough to build it into a standard.

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 aerospace and space systems worldwide — has not needed to acknowledge, being too busy running correctly to concern itself with the question of whether it is appreciated.