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.¹ 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.²

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

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.

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

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

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

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

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

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

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.¹⁰

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.

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.