沉默的巨人——Ada 编程语言的设计哲学与深远影响

文章概述

本文深入探讨了 Ada 编程语言的非凡历史及其对现代软件工程的深远影响。诞生于上世纪 70 年代末美国国防部的项目，Ada 从一开始就被设计用于解决大规模、高可靠性系统中的软件危机。文章指出，尽管 Ada 长期被业界贴上冗长、晦涩的标签并遭到边缘化，但它在模块化（包系统）、强类型（受限类型和变体记录）、泛型、内置并发控制（CSP模型）以及契约式编程等方面的设计，出奇精准地预判了软件工程的未来。在随后的 40 年里，从 C++、Java 到 Go、Rust 和 C#，几乎所有现代主流语言都在沿着 Ada 曾经的足迹，逐步“重新发现”并实现了它早在 1980 年代和 1990 年代就已经标准化的安全特性。文章不仅是对 Ada 被低估的历史地位的平反，更是对现代编程语言演进轨迹的一次深刻反思。

专用词语翻译列表

英文原词 / 术语	中文翻译	词义说明
Ada	Ada	本文讨论的核心编程语言，以第一位程序员 Ada Lovelace 命名。
Generics	泛型	一种允许延迟指定数据类型的编程机制，提高代码复用性。
Package	包	Ada 中用于模块化和封装的代码组织单元。
Concurrency	并发	计算机系统中多个任务在同一时间段内交替执行的特性。
Interface and Implementation	接口与实现	软件设计原则，将模块对外暴露的声明（接口）与其内部工作细节（实现）分离。
Discriminated Union / Variant Record	可辨识联合 / 变体记录	一种数据结构，其实例的字段构成由一个“判别式（Discriminant）”变量的值决定。
Rendezvous	汇合 / 同步通信	Ada 中的并发任务间同步传递消息的机制。
Protected Object	受保护对象	Ada 95 引入的机制，用于安全地管理并发任务间的共享状态。
SPARK	SPARK	Ada 的一个正式验证子集，专为高完整性系统设计。
Design by Contract (DbC)	契约式设计	强调软件组件间必须通过明确的前提条件、后置条件和不变量来协作的设计方法。
Exception Handling	异常处理	程序在运行时处理错误的机制。
Duck Typing	鸭子类型	一种动态类型风格，关注对象的行为（方法和属性）而非其确切的类型。
Borrow Checker	借用检查器	Rust 语言的核心特性，用于在编译期确保内存安全和防止数据竞争。

沉默的巨人——Ada 编程语言的设计哲学与深远影响

有一种语言，它让泛型成为广泛部署的系统级语言中一等公民的标准特性；它将“包（Package）”的概念规范化；它将并发机制内置于语言规范而非依赖库来实现；它强制要求接口与实现分离；它引入了范围受限类型（Range-constrained types）、可辨识联合（Discriminated unions），以及一种 Go 语言在三十年后通过不同路径独立得出的一致的任务通信模型。在随后的修订中，它又加入了受保护对象（Protected objects）、编译期非空保证以及语言级别的契约（Contracts）。

这是一门 Rust 花了十年时间从一个方向向其靠拢，而 Python 从另一个方向向其靠拢的语言；这也是一门 C# 在过去近二十年里，一个特性接一个特性地在不断逼近的语言。然而，这却也是一门被业界始终描述为冗长、晦涩且无关紧要的语言。但令人尴尬的是，那些关于软件如何进步的常见叙事往往忽略了：正是这门语言，以一种非同寻常的精确度，预见并实现了如今每一种现代语言都在努力获取的安全特性。

Ada 并不出名。它不是充满激情的会议演讲或令人屏息的博客文章的主角。它没有一个会在主题演讲中大谈编程哲学的魅力创始人，也没有一个热衷于编写框架或发布有着巧妙名称的包的社区。它所拥有的是：自 1983 年以来经过四次修订的正式国际标准；在许多大型商业飞机和航空电子系统软件中的核心地位；在上世纪 70 年代末政府合同下做出的一系列设计决策（而行业内其他人花了四十年时间才独立重新发现这些决策）；以及在了解它的程序员群体中，作为“说‘不’的语言”的声誉——它的编译器强制执行合法性、可见性、类型检查以及极高程度的安全检查（大多数语言把这些留给了约定俗成或外部工具），它要求程序员必须准确命名他们的意图，并将歧义视为错误而非特性。在很长一段时间里，这些特质被认为是它的弱点。但经得起推敲的是，这些正是目前所有被称为“现代”的语言正在试图获取的精确特质。

为何会有 Ada？一场采购危机催生的革命

要理解 Ada 为什么存在，需要了解催生它的那场特定危机——那不是计算机科学的危机，而是采购的危机。上世纪 70 年代初，美国国防部（DoD）在试图对运行在其武器系统、物流基础设施和指挥控制设备上的软件进行普查时遇到了这个问题。普查的结果并非发现了软件上的“单一种植（Monoculture）”。恰恰相反，他们发现在国防部的系统中，正在积极使用的独立编程语言和方言多达 450 多种，每一种都与特定的承包商或特定的开发时期相关联，没有一种能与其他语言互操作，除了最初的作者之外，大多数都无法被任何人维护，而那些作者很多都已经找不到了。^1 制导导弹的软件无法由维护船舶导航软件的人来维护。调度物流的软件无法与处理通信的软件共享代码。这些语言就像技术债务一样累积着：无形地、渐进地，每一个单独的决定在局部看起来都是合理的，但汇总起来却是一场灾难。

对于一个政府机构来说，国防部的回应异常成熟。它没有简单地强制规定使用现有的某种语言——COBOL、Fortran 和 PL/1 都曾被考虑过并被拒绝——而是开展了一个持续五年的需求征集过程，并产生了一系列精度不断提高的文件：稻草人（Strawman）、木人（Woodenman）、锡人（Tinman）、铁人（Ironman），最后是钢人（Steelman），每一份文件都在完善和收紧国防部编程语言必须具备的规范。《钢人》文件发布于 1978 年，是一份非凡的工程需求文献：它没有指定一种语言，而是描述了一种语言必须具备的属性——这些属性直接衍生自国防部现有软件资产的实际故障模式。它要求有一个明确分离接口和实现的模块系统。它要求具有强大的静态类型，不允许类型之间的隐式转换。它要求内置对并发任务的支持。它要求有一致的异常处理机制。它要求语言独立于机器。它要求程序能够被其作者以外的人阅读。它要求语言使程序验证变得容易。这些不是理想化的偏好。它们是从那些缺乏这些特性的程序所导致的后果中推导出来的硬性要求。^2

1979 年，在四个入围团队（分别代号为绿、红、蓝、黄）的竞争中，产生了获胜者：由 Jean Ichbiah 在法国 CII Honeywell Bull 领导的团队设计的“绿色”方案。获胜的设计被命名为 Ada，以纪念奥古斯塔·阿达·金，洛夫莱斯伯爵夫人（Augusta Ada King, Countess of Lovelace）——这位 19 世纪的数学家写下了通常被认为是第一个旨在用于机械计算的算法。这个名字的选择是经过深思熟虑的：国防部想要一个名字而不是首字母缩写，想要纪念一位在庆祝女性极少的领域中的女性，并希望传达出这种语言是意图的宣言，而不是委员会妥协的产物。Ichbiah 非常认真地对待这项任务，他为标准附带了一份基本原理文档（Rationale Document）——对每一个设计决策及其背后的推理进行了全面解释——对于任何读过它的人来说，这至今仍是关于“编程语言设计究竟是为了什么”存在的最清晰的阐述之一。

真正的封装：包规范与私有类型

Ada 架构的核心是包（Package）：一个由规范（Specification）和主体（Body）组成的编译单元，它们在物理上是分开的，编译器强制执行它们之间的关系。规范是契约——它声明了包提供的内容：类型、子程序、常量，以及包向外界提供的任何内容。主体是实现——它提供了履行契约的代码。规范是客户端代码能看到的。主体对客户端代码是不可见的，可以独立编译，可以在不重新编译任何仅依赖于规范的内容的情况下进行更改，并且可以在没有任何客户端知道或关心的情况下被完全替换。这种分离不是一种风格建议。它不是由代码检查工具（Linter）强制执行的。它是语言的一种结构属性：客户端代码试图访问未在规范中声明的任何内容都将无法编译，因为编译器不允许它看到主体。^3

这就是在 Ada 之后出现的每一种语言都在试图构建的模块系统。Java 的包不是这样的：它们是带有访问修饰符的命名空间机制，但实现对于反射、子类以及同一包内可能未被预料到的代码是可见的。Python 的模块不是这样的：它们是文件，接口和实现之间没有正式的分离，没有编译器来强制执行边界。JavaScript 的模块系统（2015 年引入，比 Ada 晚了 32 年）提供了 import 和 export，但没有提供一种机制让类型具有对其导入者隐藏内部表示的规范。C 语言的头文件近似于这种分离，但没有一个编译器能验证头文件和实现之间的一致性，也无法防止实现的细节通过预处理器宏泄漏。Go 语言的导出标识符（大写名称可见，小写名称不可见）达到了类似的效果，但没有正式的规范-主体区分。Rust 带有 pub 可见性规则的模块系统同样是一种近似。所有这些都不是 Ada 的包系统，因为它们都没有使这种分离在结构上如此彻底：在 Ada 中，私有类型的实现不仅是不可访问的，它在客户端眼中的世界里，在语法上就是不存在的。就客户端而言，它不存在。没有什么可以访问、反射或规避的。

Ada 的包规范不是一种约定。它是由编译器强制执行的契约，编译器甚至拒绝让客户端知道实现的存在。

私有类型（Private type）机制自然地从包架构中衍生出来，它赋予了 Ada 一些其他语言花了几十年时间才近似实现的东西。在 Ada 包规范中声明为私有（Private）的类型，按名称是可见的——客户端代码可以声明该类型的变量，将它们传递给子程序，从函数中返回它们——但它的内部表示是完全不透明的。客户端不知道该类型是记录、数组、整数、指针还是任何其他东西。它不能访问字段，因为它不知道存在字段。它不能以设计者未打算的方式复制该值，因为它不知道该值是如何布局的。包的设计者决定该类型存在哪些操作，在规范中声明它们，世界上其他地方只能使用这些操作。这不同于 Java 中 private 关键字意义上的访问控制，后者在防止直接访问的同时，却将内部表示留给继承、反射以及编译器在检查子类兼容性时去察觉。它是表示层面的不可见性：该类型的结构在字面上不会出现在客户端编译所针对的代码文本中。

C# 花了其存在的大部分时间来提供访问修饰符，然后才缓慢地通过诸如 record 类型、仅初始化（init-only）属性和密封类（sealed classes）等机制构建出真正的封装。Java 向着真正的数据隐藏演进的过程也类似：记录（Records）在 2021 年的 Java 16 中出现，提供了一种表示形式固定且访问器自动生成的类形式——这比 Ada 将内部表示隐藏作为任何声明为私有类型的默认设置晚了 38 年。面向对象语言向 Ada 包系统演进的旅程，就像是人们被告知访问修饰符就是封装，然后逐渐发现它们并非如此，并从头开始重建 Ada 从一开始就提供的东西。

表达领域语义的类型系统

在 1983 年，Ada 的类型系统在生产使用中是独一无二的，并且在其本质上，仍然比今天存在的大多数语言更具表现力。组织它的核心区别在于类型（Type）和子类型（Subtype）之间——不是在面向对象意义上的一个类型扩展另一个类型，而是在数学意义上的一个受限集合。如果一个 Ada 程序员需要一个代表人的年龄的类型，他们不会去拿一个 int 然后加上注释。他们会写 type Age is range 0 .. 150，然后编译器无需进一步指示，就会生成一个类型。该类型的值必须在这个范围内，它的算术运算在运行时会根据这个范围进行检查（除非程序员显式选择加入未检查的运算），并且它是一个与程序中所有其他整数类型不同的类型，因此在需要年龄的地方传递日历年份会是一个编译时错误，而不是运行时的意外或无声的错误答案。^4

这并不是增量式的改进。在 1983 年的格局中，C 语言有 int、short 和 long，通过大小和有无符号来区分，而不是通过意义。Fortran 有 INTEGER 和 REAL。Pascal 有序数子类型，但没有带有语义约束的、命名的独立类型。Ada 的范围类型、枚举类型和定点类型赋予了程序员在类型系统中直接编码意义的能力——使类型成为对值可以是什么的、由机器检查的规范。Rust 的 u8、i32、u64 是大小和有无符号的区别，防止了某些错误；Ada 的范围类型是语义约束，防止了不同的、更特定于领域的错误。Haskell 的 newtype 包装提供了一种密切相关的机制，通过不同的路径到达了 Ada 的目的地。TypeScript 的 branded types（一种涉及幻像类型参数的变通模式，被广泛使用正是因为 TypeScript 的结构类型系统会把所有整数合并在一起）的存在，就是为了解决 Ada 在 1983 年命名并解决的问题。

Ada 的可辨识记录类型（Discriminated record types）意义更为重大。可辨识记录是一种带有变体字段的记录类型——其值决定了存在哪些其他字段的字段。一个形状（Shape）可能有一个在圆形和矩形之间选择的判别式；圆形有半径字段；矩形有宽度和高度字段；编译器知道对于哪个判别式值存在哪些字段，并且不会编译访问矩形半径的代码。这就是代数数据类型（Algebraic data type）、和类型（Sum type）、标记联合（Tagged union）——函数式程序员几十年来一直倡导的作为对可以是多种事物之一的数据进行建模的正确方法。Haskell 将其作为其类型系统的核心。Rust 带有数据字段的 enum 恰好是一个可辨识联合，使用与 Ada 提供的相同的编译器保证来实现。Swift 有相关值枚举（Associated value enums），原因相同。Kotlin 有密封类（Sealed classes）。TypeScript 有可辨识联合类型（Discriminated union types），在 2016 年的 2.0 版本中加入。Ada 在 1983 年就有了可辨识记录类型，具有编译器强制的字段访问检查，并能够将它们用作其他类型的判别式，形成任意复杂的结构。过去二十年里增加和类型的每一种语言，都以自己的语法，增加了 Ada 设计者在最初标准中加入的东西。

Ada 的可辨识记录就是代数数据类型。过去二十年里增加和类型的每一种语言，都独立地重新得出了 1983 年的设计决策。

泛型：参数化多态的先驱

在 Ada 的众多贡献中，其泛型（Generic units）或许是对业界影响最直接，但也最一致地未被承认的一个。Ada 中的泛型是一个参数化的包或子程序——一个可以用特定类型或值实例化的模板，以生成具体的包或子程序。一个通用的排序过程（Generic sort procedure）接受一个类型参数、一个数组类型参数和一个比较函数参数；它可以被实例化为对整数、字符串或任何可以提供比较函数的类型进行排序。这就是参数化多态（Parametric polymorphism）：编写一次代码并将其应用于许多类型，由编译器验证每个实例化的正确性，而不是将检查推迟到运行时或依赖于鸭子类型（Duck typing）。Ada 在 1983 年就拥有了它。

C++ 大约从 1990 年开始有了模板。Java 直到 2004 年（比 Ada 晚了 21 年）才有了泛型，而且当 Java 的泛型到来时，它们是通过类型擦除（Type erasure）实现的，这意味着类型参数在编译时存在，但在程序运行前被移除，这就阻止了 Ada 泛型所提供的那种运行时类型特化。C# 在 2005 年获得了泛型，它有一个更完整的实现，在运行时保留了类型信息——更接近 Ada，但晚了 22 年。Go 语言直到 2022 年的 1.18 版本才有了泛型（比 Ada 晚了 39 年），在 Go 使用的头十年里，它们的缺席被广泛体验为一个重大限制。Rust 拥有单态化（Monomorphisation）的泛型：泛型类型的每次实例化在编译时都会产生一个具体类型，这正是 Ada 采取的方法。Rust 泛型探索的设计空间，早在 1983 年的 Ada 标准中就已经绘制出来了。^5

Ada 的泛型形式参数比大多数现代泛型系统更具表现力。Ada 中的泛型单元不仅可以接受类型作为参数，还可以接受子程序——你可以将一个函数作为形式参数传递给一个泛型，并让编译器验证它是否具有正确的签名——还可以接受包，这使得一个泛型可以由一个完整的模块而不仅仅是一个类型来参数化。这是另一种途径的更高阶多态：不仅对值进行抽象，而且对类型构造器和模块结构进行抽象。Haskell 的类型类（Type classes）通过不同的机制达到了相似的表现力。Rust 的 trait 系统正在接近它。C++ 的概念（Concepts），在 2020 年的 C++20 中加入，允许对泛型类型参数施加操作要求——这正是 Ada 的泛型形式类型参数一直以来的规范。Ada 的特性与 C++ 采用相同想法之间这 40 年的差距，在这个故事中并不罕见。

被忽视的并发模型：从汇合到保护对象

Ada 的并发模型展示了 Ada 设计与行业接受度之间的巨大差距，并且这种行业对其模型的忽视，直接导致了业界在 2000 年代和 2010 年代试图解决的并发危机。这场危机——由于多核处理器导致的共享可变状态灾难，以及基于锁的同步机制产生的死锁和测试无法可靠检测出的竞态条件——并非不可预见。具体而言，它被 Ada 的设计者们预见到了。他们在 1983 年围绕它进行了设计，并在 Ada 95 中产生了一种并发模型，而随后的语言一直在试图逼近这种模型。

Ada 的任务（Tasks）是语言级别的构造：用 task 声明，由 Ada 运行时调度，通过汇合（Rendezvous）或受保护对象（Protected objects）进行通信。汇合是一个同步通信点：一个发起调用的任务命名它希望使用的入口（Entry），一个接受任务在 accept 语句中命名相同的入口，只有当双方都准备好时，它们才能继续执行。通信发生在相遇时；任务永远不会隐式共享内存；调用任务无法进入接受任务并修改其状态，因为通信模型根本没有提供这样做的机制。这就是消息传递（Message passing）——不是指将一个值序列化并通过套接字发送，而是指通信的设计在构造上就阻止了对共享状态的访问。Go 的通道（Channels）正是这一理念的一种直接实例化，只是语法不同，语义稍有区别。Go 的设计者通过仔细思考并发安全性得出了通道；Ada 的设计者通过同样的路径，在 30 年前得出了汇合。^6

Ada 95 的受保护对象（Protected objects）解决了真正需要共享状态的情况。受保护类型包装数据并声明对其进行的操作：受保护过程（具有独占读写访问权限）、受保护函数（因为它们是只读的，所以可以并发调用），以及受保护入口（类似于过程，但包含一个屏障条件，即操作继续进行必须为真的布尔表达式，调用任务会自动挂起，直到条件满足）。运行时对过程和入口强制执行互斥，程序员无需编写锁。每当任何操作完成时，入口的屏障条件都会重新评估，从而提供了一种安全的条件等待，而无需 Java 并发模型中要求的手动条件变量信号机制。Rust 的 Mutex 和 RwLock 类型以相关的方式保护数据（将状态包装在强制执行访问纪律的类型中），但这是通过库而不是语言构造来实现的，并且没有屏障条件机制。Java 的 synchronized、wait 和 notify 是程序员常用的工具，但它们的组合很容易引发微妙的错误：忘记同步、通知了错误的条件、在持有锁时调用外部代码。Ada 的受保护对象使得这些错误在结构上不可用，而不仅仅是不鼓励。

SPARK 作为 Ada 的一个子集，将并发保证扩展到了形式证明（Formal proof）的高度。SPARK 排除了任务可访问状态之间的别名，将子程序中的副作用限制为子程序契约中声明的那些，并提供了一个静态分析工具链。它能够在数学层面而非经验层面证明，一个程序没有数据竞争、没有未处理的异常、没有越界数组访问，也没有违反陈述的前置条件和后置条件。Rust 的借用检查器在编译时防止了一类内存安全错误，这是一个相关但范围更窄的保证：它防止了释放后使用、双重释放和某些形式的别名修改，但它并不正式证明程序的逻辑正确性。SPARK 则同时证明了内存安全和逻辑。Rust 在编译时拒绝不安全程序与 SPARK 形式证明正确程序之间的差距，就是工程纪律与数学验证之间的差距——而 SPARK 在生产系统中占据后者的位置，早于 Rust 作为项目的存在。^7

Go 的通道和 Ada 的汇合是在更广泛的 CSP 传统中的近亲。Rust 的借用检查器防止了 SPARK 所证明内容的一个子集。行业花了三十年时间向着 Ada 从一开始就标出的立场汇聚。

契约式设计与编译期安全保障

Ada 2012 为语言增加了契约（Contracts）：前置条件（Preconditions）、后置条件（Postconditions）和类型不变量（Type invariants），它们用 Ada 自己的语法表达，并由编译器或在程序员的指示下由运行时进行检查。一个子程序的前置条件是一个布尔表达式，在调用子程序时必须成立；它的后置条件是一个布尔表达式，在它返回时必须成立；类型不变量是一个属性，每当该类型的值对外部代码可见时，它都必须成立。这些不是可能在生产中被禁用的运行时检查意义上的断言。它们是规范：机器可读的、关于子程序需要什么和保证什么的声明，SPARK 工具链可以验证这些声明，而完全无需执行程序。^8

契约式设计（Design by Contract）——这个由 Bertrand Meyer 在 1986 年的 Eiffel 语言中命名并系统化的想法——是这一机制的概念基础。Eiffel 首先拥有了它；Ada 2012 在一种拥有庞大现有用户群、正式标准和验证工具链的语言中将其形式化，该工具链能够利用契约进行静态证明，而不仅仅是运行时检查。这个想法在更广泛的行业中的发展轨迹一直很缓慢。尽管提案可以追溯到 2010 年代初，C++ 至今没有标准的契约机制；C++20 推迟了准备多年的契约提案。Java 语言中从未有过契约；Java 中的 DbC 是通过库、Javadoc 约定或通过近似后置条件检查的 JUnit 测试来完成的。Python 的类型提示（Type hint）系统，在 2015 年的 3.5 版本中引入并随后逐步扩展，是对契约的一种部分尝试：它指定了输入和输出的类型，但没有指定行为属性。Rust 的 trait 边界（Trait bounds）和类型约束（Type constraints）是另一种部分尝试。这些都没有提供 Ada 2012 所提供的：一种标准的、编译器集成的符号，用于声明子程序需要什么和保证什么，在开发过程中的运行时可检查，并由随语言附带的工具链静态证明。

每一种主流语言的演进方向都是向着契约迈进。TypeScript 的类型系统在每个版本中都变得更具表现力，增加了条件类型（Conditional types）、模板字面量类型（Template literal types）和越来越细粒度的类型收窄（Narrowing）——所有这些都是具有契约能力的类型系统所能直接表达的内容的近似。Python 的 typing 模块在每个版本中都在增长，增加了 Protocols、TypedDict、ParamSpec 和 Concatenate——逐步构建出那种 Ada 自 1983 年以来就拥有的接口规范。C# 的可空引用类型（Nullable reference types），在 2019 年的 8.0 版本中加入，施加了 Ada 从一开始就施加的访问类型设计约束：必须显式声明引用可空以允许空值，并且编译器强制执行该区分。可空引用危机（空指针作为十亿美元的错误，Tony Hoare 自称最糟糕的设计错误）是一个 Ada 减轻了但没有解决的危机。Ada 的访问类型（Access types，即指针）默认初始化为 null，并且取消引用空访问值会在运行时引发 Constraint_Error——一种已定义的行为，不同于 C 语言在空取消引用时的未定义行为，但这是一个运行时检查而不是编译时保证。Ada 2005 引入了 not null 访问类型注释，允许程序员声明特定访问值可能永远不为空，并让编译器静态地强制执行该限制。这是真正的编译时空安全，但它是需要选择性加入（opt-in）的，是在原始标准发布 22 年后添加的，并且不是默认设置。C# 在 2019 年 8.0 版本中添加的可空引用类型采取了相反方向的选择性加入方法：除非显式注释为可空，否则假定引用非空。这两种语言都得出了相同的架构洞察——可空性应该在类型中可见——但都没有从一开始就将其作为默认设置，也都不能声称已经消除了 Hoare 指出的那个问题。Ada 从一开始提供的是更安全的故障模式：引发异常而不是破坏内存。

结构化异常处理的基础奠定者

Ada 在 1983 年引入的异常处理模型，是结构化异常处理（Structured exception handling）的首次生产级实现——这种理念认为，异常不只是简单跳转到错误处理程序，而是作为一种事件被引发，通过预定义的调用栈传播，并在与触发它的代码块或子程序语法上相关联的异常处理程序中进行处理。Ada 的模型要求异常必须先声明再使用，处理程序必须与特定作用域相关联，并且传播规则必须被精确定义。C++ 在 1990 年采用结构化异常处理，比 Ada 晚了 7 年。Java 在一个重要方面比 Ada 走得更远：Java 的受检异常（Checked exceptions）要求某些异常类型必须被捕获，或者在方法的 throws 子句中声明，这使得调用者处理失败的责任成为该函数编译接口的一部分。Ada 没有类似的机制——Ada 的异常在调用栈中自由传播，子程序的规范并未说明它可能引发哪些异常。Java 的受检异常与其说是从 Ada 借鉴，不如说是更多受到了 CLU 的信号机制（Signalling mechanism）和 Modula-3 的异常声明启发。而且这一实验从一开始就充满争议：受检异常被广泛认为是 Java 设计上的失误之一，Scala 和 Kotlin 完全移除了它们，而业界也从未就“编译器是否应该在调用点强制执行异常感知”这一问题达成共识。^9

Rust 做出了一种相关的选择，即完全移除异常：错误是值，通过包含在 Result 类型中从函数返回，函数是否会失败的问题表达在它的返回类型中，而不是在单独的异常机制中。这是对同一个潜在问题（即调用者必须知道被调用的函数是否可能失败以及以何种方式失败）的不同解决方案，它得出结论是 Ada 的异常模型没有得出的：在 Ada 中，与 C++ 和 Python 一样，异常是一个隐藏的通道，它在调用栈中传播而不出现在子程序的规范中，调用者可以完全忘记它们，直到它们发生。Rust 的“错误即值”方法和 Java 的受检异常是两次试图关闭该通道的尝试。Ada 的贡献不在于关闭它，而在于将其结构化——用一种传播规则已定义、处理程序具有作用域、行为可预测的机制，来取代 setjmp/longjmp 的原始跳转和信号处理程序的模糊性。这种结构化是之后每个异常系统建立的基础，甚至是那些走得比 Ada 更远的系统。

“契约标准”：独一无二的 Annex 附件模型

Ada 的附件（Annexes）——在标准中定义的对核心语言的可选扩展，需要单独的编译器认证——代表了一个没有任何其他语言复制过的设计决策，如果业界能够考虑它，或许会从中受益。这些附件为特定领域定义了功能：实时系统、分布式系统、信息系统、数值计算、安全与保障、高完整性系统。一个实现了附件 C（用于系统编程）的编译器必须实现某些预定义的属性和表示子句。一个实现了附件 D（用于实时系统）的编译器必须以标准指定的方式实现任务优先级、调度策略和时间约束。编译器符合某个附件的认证是可独立验证的。编译器的用户确切知道它支持什么和不支持什么，因为这种支持是针对正式标准的一项记录在案的、可测试的声明，而不是编译器作者决定实现的那些自发属性。^10

没有其他主流语言有这种模型。JavaScript 的特性支持是通过兼容性表来追踪的，因为标准和实现是两个分离的世界，没有正式的耦合。Python 的标准库覆盖范围因实现而异——CPython、PyPy 和 MicroPython 都是自称为 Python 的不同东西。Rust 的特性集有正式的稳定版或不稳定版，但这二者之间的界限会随时间移动，并且不存在可认证合规性的概念。C++ 编译器竞争的是它们实现了最新标准的哪些功能，而不是对任何已定义子集的经过认证的合规性。Ada 的附件模型传递的理念是，标准应该是一份契约——可测试的、可认证的。它之所以有用，正是因为它不仅说明了什么是被允许的，还说明了什么是被要求的。管理每架获得认证的民用飞机软件的 DO-178C 机载软件认证标准，要求提供文档和过程证据。如果使用具有可认证编译器一致性的正式标准化语言，生成这些证据要容易得多。Ada 的标准及其附件结构和一致性测试方案，异乎寻常地直接契合了 DO-178C 的要求。C 和 C++ 也能满足相同的认证要求——而且确实经常这么做——但那是通过额外的过程文档和工具，而不是通过一个在设计时就考虑到认证的标准。Ada 的标准化和工具使其非常适合需要大量认证的领域；这并不意味着它是唯一能在这些领域运作的语言。

被忽视的深层原因：文化、美学与“幸存者偏差”

为什么 Ada 的影响力如此一致地不被承认？这个问题有几个答案，但没有一个能令人完全满意。

最直接的原因是体制上的：Ada 是一种政府语言，通过一个硅谷没有关注、即使关注也不会尊重的流程采购而来。C++、Java 和 Python 的设计者并没有阅读《钢人》文件。他们只是在解决面前的问题——让 C 语言更安全，让软件对象起作用，让脚本编写变简单——而他们的解决方案与 Ada 的解决方案趋同，不是因为他们在效仿 Ada，而是因为面对的是相同的问题，优秀的解决方案终究是相似的。

第二个答案是美学上的。Ada 的语法对于有 C 语言背景的程序员来说，显得繁琐且令人不悦。它使用 if X then Y; end if; 而不是 if (x) { y; }；使用 procedure Sort (A : in out Array_Type) 而不是 void sort(int* a)。这种繁琐是刻意为之的——Ichbiah 希望程序能被作者以外的人阅读，而在时间跨度下，可读性需要明确性——但它被认为是官僚主义和非黑客做派的。形成于 1980 年代和 1990 年代的编程文化的核心主张是：简洁即高级。Ada 是采购官员的语言。C 是懂得机器的人的语言。这种文化判决很早就做出了，并且从未被实质性地重新审视过。

第三个答案是，Ada 的部署领域决定了它的成功是不可见的。一个编译无误、运行没有竞态条件、并且已被正式验证满足其规范的软件项目，不会产生事故报告，不会有事后分析（Post-mortems），也不会有关于什么出错了的会议演讲。Ada 的成功——没有坠毁的飞机、没有故障的铁路信号系统、没有偏离轨道的导弹制导软件——正是因为它们是成功，所以不可见。那些因为缓冲区溢出、空指针异常、数据竞争和安全漏洞而明显失败的语言，引发了无尽的讨论。Ada 产生了可靠的软件，而可靠的软件并不能产生话题和流量。

Ada 的成功因为其成功本身而不可见。那些明显失败的语言引发了广泛的讨论。可靠的软件不会产生会议演讲。

结语：现代语言的归途，竟是 Ada 的来路

现代语言设计的轨迹，如果仔细追溯，就是一条朝着 Ada 早已占据的位置前进的轨迹。Rust、Haskell、TypeScript 和 Swift 因之备受赞誉的类型系统特性——和类型、参数化多态、基于约束的泛型、仿射类型（Affine types）和所有权——每一个都解决了一个 Ada 在 1983 年就发现了的问题，而随后 20 年里的主流语言却拒绝解决这些问题。Go、Rust 和 Swift 因之受到赞扬的模块系统——明确的接口、规范与实现的分离、编译器强制执行而非仅仅建议的可见性控制——是对 Ada 从一开始就提供的包系统的部分实现。为 Go 的通道和 Rust 的所有权带来赞誉的并发模型，与 Ada 的汇合及受保护对象模型属于相同的 CSP 和消息传递谱系，后者在 1983 年和 1995 年为相同问题提供了生产级的答案。C# 的可空引用、TypeScript 的类型收缩和 Python 的渐进类型（Gradual typing）从不同角度正在逼近的契约系统，正是 Ada 2012 添加到这门从今天大多数从业者出生前就已持续使用的语言中的东西。

这并不是说每一种现代语言都在抄袭 Ada，或者 Ada 的设计者应该获得那些被隐瞒的荣誉。大部分的趋同都是真正独立的：Rust 的设计者并没有从 Ada 的访问类型规则中推导出借用检查器；Go 的设计者并没有从 Ada 的汇合中推导出通道；TypeScript 的设计者也没有从 Ada 的变体记录中推导出可辨识联合。这种趋同是真实的，但它是朝着实际问题的正确解决方案趋同，而不是剽窃。Ada 的设计者最先发现了这些问题，并以非同寻常的清晰度识别出了它们，因为他们当时设计语言所处的背景是：这些问题已经导致了人员死亡，如果解决方案错误，还会导致更多人死亡。

Ada 所展示的，不是它应该被更广泛地使用——尽管在任何关心软件可靠性的领域中使用它的理由，都比业界给予它的认可要充分得多——而是，现代语言设计正在解决的问题是老问题，现代语言正在发现的解决方案也是老解决方案。

认为空引用需要明确的注释、并发需要语言级别的强制约束而非库级别的约定、接口和实现应该在结构上分离、类型系统应该编码领域约束而不仅仅是机器表示、泛型代码应该在实例化时可验证——这些洞见都不属于 2010 年代或 2020 年代。它们是 1970 年代和 1980 年代的洞见。这些洞见的形成，是对那些产生过具体严重后果的软件故障的回应，严重到负责预防这些故障的人愿意为一场持续五年的语言竞赛买单。

在过去 40 年里，业界花费巨大精力构建各种新语言，它们最优秀的特性都在独立地向着 Ada 几十年前就占据的立场靠拢；同时，业界也花费了同样的 40 年来形容 Ada 是一门“无关紧要”的语言。这两个事实之间存在着一种连业界尚未完全承认的张力。

但 Ada 不需要这份承认。它被部署在头顶呼啸而过的客机里，部署在铁路沿线的信号系统中，部署在穿梭于星际间的宇宙飞船制导系统里。它正忙于精准无误地运行，根本无暇顾及自己是否受到了足够的重视。

脚注

[1] 国防部软件危机被记录在 1970 年代初的一系列内部研究中，并在 1974 年的报告《高级计算机编程语言的需求》（Requirements for High Order Computer Programming Languages）中进行了总结。该报告确定了在整个国防部系统中使用的 450 种语言和方言，并估计软件成本正以不可持续的速度增长。450 种语言这个数字在多篇关于 Ada 开发过程的历史文献中被引用，包括 Jean Sammet 和 Fred Neighbors 在 1986 年《ACM 通讯》上发表的《ADA 编程语言》（"The ADA Programming Language"）。促成这项竞赛的具体成本预测则详细记录在 David A. Fisher 1976 年的《一种适用于国防部的通用编程语言》（"A Common Programming Language for the Department of Defense"）一文中。
[2] 《钢人》文件——正式名称为《高级计算机编程语言的需求 (Steelman)》，发布于 1978 年 6 月——是一系列需求文档中的最终版。它的早期版本分别被称为“稻草人”（Strawman, 1974）、“木人”（Woodenman, 1975）、“锡人”（Tinman, 1976）和“铁人”（Ironman, 1977）。这些文件可以从公共档案中获得，非常值得一读：从“稻草人”到“钢人”的演变过程，记录了需求在经验中不断被完善的历程，而《钢人》的最终版本在关于它要求什么以及为什么要求方面显得特别精确。1979 年提交的四份竞争设计方案由独立团队根据《钢人》的需求进行了评估。所有四种设计都通过了初步评估；“绿色”和“红色”进入了最终评估；“绿色”方案最终入选。负责管理这场竞赛的高级语言工作组（High Order Language Working Group）由 Jean Sammet 担任主席。
[3] Ada 的包结构在《Ada 参考手册》(ARM) 第 7 章中有规定。规范和主体的分离在编译时被强制执行：包主体必须与其规范一致，且针对规范编译的客户端代码无法看到主体。包规范中的私有部分——位于 private 关键字和规范的 end 之间——在编译客户端代码时对编译器是可见的（以便编译器能够为私有类型对象分配存储空间），但在语义上是不可用的：客户端代码不能引用任何仅在私有部分定义的内容。Ada Rationale (Ichbiah et al., 1979) 将这种设计解释为明确拒绝那个时代系统语言中常见的公共字段模式。
[4] Ada 的类型系统（包含类型与子类型的区别，以及对范围约束、枚举类型、定点类型和模块类型的支持）在 ARM 的第 3 到第 5 章中进行了描述。这种设计原则——即类型是值的集合和操作的集合，且不同的语义域需要不同的类型，即使它们的内部表示是相同的——在 Ada Rationale 中得到了明确阐述。这部分归功于 Barbara Liskov 的 CLU 语言的影响，部分归功于国防部的一项操作要求，即混合使用不同单位（如英尺和米、磅和千克）的程序必须在编译时被检测出来。1996 年的阿丽亚娜 5 号（Ariane 5）火箭灾难，就是因为在发射后 37 秒，一个 64 位浮点数在没有进行范围检查的情况下被转换为 16 位整数，导致火箭坠毁。这个错误发生在 Ada 代码中，该代码使用了“未检查的转换（unchecked conversion）”绕过了 Ada 的类型系统。这场灾难有时被认为是 Ada 的失败；但更准确地说，它是展示当 Ada 的类型检查被显式绕过时会发生什么的一个反面教材。
[5] Ada 的泛型单元在 ARM 的第 12 章中定义。泛型形式参数可以是类型（带有不同程度的约束）、子程序、对象或包。将包作为泛型参数传递的能力——一种高阶多态的形式——在 Ada 83 中就已经存在，并在随后的修订中得到了完善。Java 决定通过“类型擦除（Type erasure）”来实现泛型——在源代码级别保留类型参数，但在编译后的字节码中将其移除——是出于向后兼容性的考虑。但这产生了一个有着各种限制的泛型系统：它无法表达需要运行时类型信息的操作，不能使用基本类型（Primitive types）作为类型参数，并且在与传统的非泛型代码交互时会产生编译器警告（unchecked cast）。C# 的具体化泛型（Reified generics）——在运行时保留类型信息——避免了这些限制；微软的设计师明确表示，他们研究过 Java 的方法并选择了一种不同的架构。但这两种方法的表现力都不如 Ada 的泛型形式参数，后者可以被约束为支持特定操作的类型，在实例化时进行检查，既没有类型擦除的问题，也不需要 Java 有界通配符（Bounded wildcards）所要求的那种名义继承（Nominal inheritance）。
[6] Ada 的任务汇合（Task rendezvous）模型在 ARM 的第 9 章中有描述。该设计受到了 C.A.R. Hoare 在 1978 年发表的“通信顺序进程（Communicating Sequential Processes, CSP）”形式主义的影响，CSP 提供了一个通过同步事件进行任务通信的数学模型。Go 语言的通道也派生自 CSP，这一点得到了 Rob Pike 的明确承认。Pike 在开发 Newsqueak 和 Limbo 语言时就运用了 Hoare 的理念，并在后来将它们贡献给了 Go。从 Hoare 的 CSP 到 Ada 的汇合，再到 Pike 的通道模型，这是一条单一的演进脉络，这使得通常将 Go 的通道描述为一种新想法的说法成为了对历史的压缩。在 Ada 95 中添加的受保护对象（Protected objects），由 Tucker Taft 等人设计，用于解决需要共享状态的情况——这是纯汇合模型处理起来比较尴尬的情况——它借鉴了早期关于监视器（Monitors）和并发对象模型的研究。
[7] SPARK Ada 最初由英国的程序验证有限公司（Program Validation Limited, PVL）开发，目前由 AdaCore 维护，其主要的静态分析工具是 GNATprove。SPARK 语言的定义独立于 Ada 标准维护，并指定了 Ada 的一个子集，该子集排除了别名（Aliasing）、不受约束的副作用以及某些形式的动态分派。GNATprove 使用抽象解释和 SMT（可满足性模理论，satisfiability modulo theories）求解器，在不执行程序的情况下，证明子程序满足其契约，数组访问不越界，整数运算不溢出，以及任务之间不存在共享状态的数据竞争。空客 A380 的主飞行控制系统、SHOLIS 直升机系统以及英国的 MULTOS 智能卡操作系统，都曾在 SPARK 中得到过形式验证。Rust 的形式验证工具集——如 Kani、Creusot 等——是研究和生产工具，对 Rust 程序应用基于 SMT 的类似验证；它们比较新，成熟度较低，而且覆盖的 Rust 特性子集比 GNATprove 覆盖的 SPARK 子集要小。
[8] Ada 2012 的契约模型在 ARM 的第 6.1 章（前置条件和后置条件）和 7.3.2 章（类型不变量）中进行了规定。前置条件和后置条件是用 Ada 本身编写的布尔表达式，当启用断言检查时，分别在子程序进入和退出时进行计算。SPARK 的工具链将相同的表达式用作形式验证的规范。Bertrand Meyer 的 Eiffel 语言在 1980 年代中期引入了“契约式设计（Design-by-contract）”这一术语，以及不变量、前置条件和后置条件的概念；Ada 2012 的契约模型在很大程度上与 Eiffel 保持一致，不过它与 SPARK 证明系统的整合，使得契约的作用超出了 Eiffel 所提供的运行时检查的范畴。C++20 的契约提案原本打算用类似的语法将前置条件和后置条件添加到 C++ 中，但在委员会对语义产生分歧后被撤回；截至 2024 年，正在为未来的标准开发修订版提案。在语言特性的历史中，Ada 的先驱设计与 C++ 采用契约之间长达 40 年的差距，如果不是最长的，也几乎是最长的了。
[9] Ada 的异常模型在 ARM 的第 11 章中定义。异常必须被声明，并且它们的传播必须通过结构化的调用栈——而不是通过 setjmp/longjmp 或信号处理程序——这是最初 Ada 83 设计的一部分。《钢人》文件明确要求“提供一种统一的机制来处理运行时错误和其他异常情况”。然而，Ada 的异常模型不包含任何声明子程序可能引发哪些异常的机制：异常自由传播，调用者没有编译器强制的责任去处理或声明它们。Java 的受检异常——要求在声明的 throws 子句中的特定异常类型必须被捕获或由调用者重新声明——超越了 Ada 的做法，更多地直接借鉴了 CLU 和 Modula-3 的异常机制。受检异常模型从一开始就在 Sun 公司内部备受争议，随后的历史——受检异常被广泛认为是一个设计错误，RuntimeException 和 Error 被用来规避检查要求，Scala 和 Kotlin 移除了受检异常同时保持 Java 兼容性——是一部业界测试并很大程度上拒绝了某个 Ada 设计者并未采取的立场的历史。
[10] Ada 的规范性附件定义在 ARM 的末尾：附件 C（系统编程）、附件 D（实时系统）、附件 E（分布式系统）、附件 F（信息系统）、附件 G（数值计算）和附件 H（高完整性系统）。编译器可以声明符合这些附件的任意子集，每一项符合性声明都必须接受独立的验证测试。Ada 符合性评估局（Ada Conformity Assessment Authority, ACAA）管理 Ada 符合性评估测试套件（ACATS），任何符合规范的 Ada 实现都必须通过该测试套件。适用于民用飞机机载软件的 DO-178C 标准（由 FAA、EASA 及同等权威机构认证）要求提供文档和过程证据，这使得更高的认证级别（设计保证级别 A 和 B）要求极高。Ada 的正式标准及其附件结构和符合性测试方案，以 DO-178C 可以直接引用的形式，提供了语言级别保证的证据。C 和 C++ 也广泛用于 DO-178C 认证的软件中，通过额外的过程文档和符合资质的工具实现同等的认证。Ada 在此背景下的优势不在于它是排他性的，而在于它的匹配度：语言标准在设计时就部分考虑到了认证机构的需求。

勘误说明

异常处理与 Java 的受检异常。 本文的初始版本指出，Java 的受检异常“直接借鉴了 Ada 的理念，即调用者应该知道子程序可能引发哪些异常”，并且 Ada 从一开始就将异常规范“作为标准功能包含在其子程序规范中”。这两个说法都是错误的。Ada 的异常模型要求将异常声明为具名对象，并且处理程序必须与特定作用域相关联，但它没有要求——也从未要求过——子程序声明它们可能引发哪些异常。Ada 没有类似 Java 中 throws 子句的机制。在 Ada 中，异常在调用栈中自由传播；调用者没有编译器强制的义务去处理或确认它们。Java 的受检异常机制超越了 Ada 所提供的范围，其思想渊源更直接地来自 CLU 的信号机制和 Modula-3 的异常声明，而非 Ada。修改后的文本反映了 Ada 的实际贡献——将异常传播结构化为一种定义明确、带作用域、行为可预测的机制——而没有过度夸大称 Ada 要求调用者知道子程序可能引发什么异常。相应的注释（9）以及关于 Rust 错误处理模型的段落已做相应修订。

访问类型与空安全（Null safety）。 初始版本指出，可空引用危机是“Ada 没有遇到的危机，因为 Ada 访问类型默认初始化为 null，并且编译器要求在使用前显式排除空值或进行空值检查”，以及“C# 在 Ada 之后 36 年才实现了强制的空安全”。这在实质上歪曲了 Ada 处理空值的语义。Ada 的访问类型确实默认初始化为 null，但对空访问值进行解引用并不会产生编译时错误——它会在运行时引发 Constraint_Error。这是一种明确且可恢复的行为（不同于 C 语言中空指针解引用的未定义行为），但并不是编译时空安全。提供编译时空排除的 not null 访问类型注解是在 2005 年的 Ada 2005 中引入的，比最初的标准晚了 22 年，且需要选择加入（opt-in）而非默认。修改后的文本描述了 Ada 实际提供的内容——从一开始就提供更安全的运行时故障模式，以及从 2005 年开始提供真正但需选择加入的编译时空排除——而没有提出“Ada 从一开始就解决了空值问题”的错误声明。

题记（Epigraphs）。 初始版本中包含三条分别归属于 Jean Ichbiah、Bjarne Stroustrup 和 Tucker Taft 的题记语录。由于无法追溯到可靠的第一手或二手来源，现已将它们移除。

“发明了泛型”。 第一段最初将 Ada 描述为“发明了泛型的语言”。在 Ada 之前就存在参数化抽象，尤其是 CLU 语言（Liskov 等人，1977 年）。Ada 使泛型成为广泛部署的系统级语言中一等公民的标准特性，这是一个不同且更站得住脚的说法。相关表述已做修改。同时，第一段压缩的时间线（原先暗示所有主要特性都在 1983 年发布）也已展开，以承认受保护对象在 Ada 95 引入、not null 在 2005 年引入、契约在 2012 年引入。

“Go 的通道就是换了语法的 Ada 汇合”。 原文中的一处引语和演进轨迹段落，都将 Go 的通道描述为对 Ada 汇合的重新实现。更准确的说法是，两者都属于源自 Hoare 1978 年形式主义的更广泛的 CSP/消息传递传统。Go 的自身谱系明确地穿过 Newsqueak 和 Limbo；它与 Ada 之间的家族相似性是真实的，但“直接等效”的说法过于绝对。修改后的文本将它们描述为在共享谱系中的近亲。

航空与 DO-178C。 初始文本称 Ada “在目前服役的每一架商业飞机的软件中都占有一席之地”，并暗示 DO-178C 实际上将 Ada 的正式标准作为先决条件，这意味着其他语言不能用于经过认证的机载软件。这两个说法都没有现有证据支持。Ada 被用于许多大型商业飞机和航空电子系统中，但“每一架商业飞机”是无法核实的，且几乎可以肯定是错误的。对于 DO-178C 认证，通过额外的过程文档和符合资质的工具，C 和 C++ 同样能常态化地达成认证；针对认证场景的 Rust 工具也正在积极开发中。修改后的文本将 Ada 的标准化和工具描述为异乎寻常地适合认证要求严格的领域，但不再声称其具有排他性。注释 10 已相应修订。

注释 3 中的“友元类（friend-class）”时代错误。 原注释将“明确拒绝 C 语言中变得普遍的 friend-class 和 public-field 模式”归功于 Ada Rationale。friend 关键字是 C++ 的特性（Stroustrup, 1985 年），而不是 C 语言的特性；它在 1979 年的语言环境中并不存在。同时，未注出来源的 Ichbiah 语录（“将私有部分作为结构性防火墙”）也已被移除。该注释现在仅提及 Ada Rationale 拒绝了那个时代系统语言中的公共字段模式，去掉了不符合时代背景的 C++ 归因。

“拒绝编译无法验证的程序的语言”。 最初的第二段将 Ada 描述为“拒绝编译它无法验证的程序的语言”。这夸大了 Ada 编译器的强制执行能力。Ada 编译器检查合法性、可见性、类型、可访问性以及许多与安全相关的约束，但完整的形式验证——证明没有运行时错误、数据竞争和契约违规——是 SPARK 和 GNATprove 的领域，而不是普通 Ada 编译的过程。修改后的文本准确描述了编译器的实际执行情况，没有将其与形式证明混为一谈。