Ada 语言的魅力 —— 用类型阐述设计，支撑运行数十年软件的语言

1. 首先要抓住的重点

你听说过 Ada 这个语言的名字吗？

可能不少人对它的印象是“老旧的语言”“军用的语言”“只在课堂上听过名字”。

但事实上，Ada 至今仍是一门在用的语言。

在民航飞机的飞行控制、铁路信号系统、火箭、空中交通管制、人造卫星、医疗设备等一旦停机就会关系到人命的软件世界里，Ada 已经被持续使用了数十年。

理解 Ada 时，重要的是下面这个视角：

Ada 是一门全力投入“在运行之前就把 bug 消灭掉”的语言
类型不是数据的容器，而是用来表达设计意图的工具
规格与实现的分离、契约、并发处理都内置在语言之中
它没有流行起来，但其设计理念被现代语言继承了下来

本文将整理 Ada 的历史、语法、强类型、范围约束、包、契约式设计、任务（task）、SPARK、开发环境，以及它的弱点，带你了解 Ada 的魅力。

希望平时写 C#、C++、Java 的读者，也能从中带走“用类型阐述设计”的感觉。

顺便一提，本文出现的代码片段，已经按章节整理成参考代码集，发布在 GitHub 上。

ada-language-appeal - komurasoft-blog-samples (GitHub)

2. Ada 是什么 —— 名字的来源与历史

Ada 是 1970 年代后期，由美国国防部（DoD）主导诞生的通用编程语言。

当时的国防部面临一个问题：每个项目使用的语言各不相同，导致软件的维护成本不断膨胀。

于是，他们通过一场国际性的设计竞赛，选出了一款也能用于嵌入式系统和实时系统的标准语言。

最终获选的，是由 Jean Ichbiah 领导的团队提出的设计方案。

语言名字 Ada，来源于被称为世界上第一位程序员的 Ada Lovelace（奥古斯塔·爱达·金，勒芙蕾丝伯爵夫人）。

大致整理一下 Ada 的历史：

1980年 制定第一版规格 MIL-STD-1815
1983年 Ada 83（ANSI 标准）
1987年 成为 ISO 标准
1995年 Ada 95（引入面向对象、受保护对象）
2005年 Ada 2005（接口、扩充容器库）
2012年 Ada 2012（把契约式设计纳入语言功能）
2022年 Ada 2022（最新标准）

Ada 95 是最早通过 ISO 标准化的面向对象语言之一。

而在 Ada 2012 中，前置条件、后置条件、类型不变式等契约式设计（Design by Contract）被纳入了语言规格。

Ada 并不是“老旧的语言”，而是一门修订超过 40 年的语言。

3. Ada 用在哪些地方

Ada 持续被使用的代表性领域，是需要高可靠性（High Integrity）的系统。

民航飞机的飞行控制与航空电子设备
空中交通管制系统
铁路的信号与联锁系统
火箭、人造卫星
国防系统
医疗设备
金融与产业界部分核心系统

这些领域有共同的特征：

bug 会直接关系到人命或造成巨额损失
认证与审计会要求“正确性的证据”
一旦部署就会持续使用数十年
事后修复的成本极高

在这样的世界里，“先发布，之后再修就好”的想法并不适用。

Ada 的语言设计，正是为了回应这样的需求。

编译期能发现的 bug 在编译期处理，只有运行期才能发现的用运行期检查处理，甚至更进一步，能用数学方式证明的就用证明来消灭——这种思路贯穿了整个语言。

这种思维方式，对写 Web 或桌面业务应用的开发者来说，也很值得学习。

4. 先来个 Hello, World

我们来看看 Ada 的代码。

with Ada.Text_IO;

procedure Hello is
begin
   Ada.Text_IO.Put_Line ("Hello, Ada!");
end Hello;

第一眼会注意到下面几点：

用 with 引入库单元
程序的主体是过程（procedure）
用 begin / end 包住代码块
end 之后要重复写一次名字
语句以分号结尾

像 end Hello; 这样在结尾重新写出名字，是很有 Ada 特色的地方。

即使代码块层层嵌套，也能一眼看出“这个 end 对应的是哪个”。

编译器也会检查名字是否对应，代码块结尾写错就会变成编译错误。

看起来是件小事，但这正体现了 Ada 的理念：“让语言撑住人容易读错的地方”。

5. 重视可读性的语法

Ada 的语法设计，可读性优先于易写性。

因为它建立在一个前提之上：软件被阅读的次数，远远多于被编写的次数。

举例来说，循环与条件分支是这样写的：

for I in 1 .. 5 loop
   Ada.Text_IO.Put_Line (Integer'Image (I * I));
end loop;

if Temperature > 80.0 then
   Start_Cooling;
elsif Temperature < 20.0 then
   Start_Heating;
else
   Keep_Current_State;
end if;

case 语句有一个很有 Ada 特色的地方：

case Today is
   when Mon .. Fri =>
      Put_Line ("Weekday");
   when Sat | Sun =>
      Put_Line ("Weekend");
end case;

要点如下：

case 没有覆盖所有值就会编译错误
不存在像 C 系语言那样隐含的 fallthrough
可以用范围（Mon .. Fri）或选项（Sat | Sun）归纳条件

只要在枚举类型里新增一个值，没有覆盖到的 case 语句就会全部变成编译错误。

“编译器会帮你列出规格变更所影响的位置”，这种体验一旦尝过就很难放手。

此外，参数还可以使用具名关联：

Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);

这能防止参数顺序搞混，调用端的代码本身就成了文档。

赋值用 :=，比较用 =，像 C 系语言 if (a = b) 那样的手误，在语法层面就不会发生。

6. 强类型 —— 把单位混淆变成编译错误

Ada 最大的魅力，就是强类型。

很多语言都会用“强类型”这个词，但 Ada 的强类型更深一层。

在 Ada 中，即使结构完全相同，用不同名字声明的类型也是不同的类型。

type Meters  is new Float;
type Seconds is new Float;

Distance : Meters  := 100.0;
Time     : Seconds := 9.58;

这两者本质上都是浮点数，但不能混着用。

Distance := Time;            -- 编译错误
Distance := Distance + Time; -- 编译错误

只有刻意要做转换时，才需要显式写出来。

Speed : constant Float := Float (Distance) / Float (Time);

为什么要严格到这个程度？

现实世界中，不少软件事故的原因都是“单位混淆”。

一个知名的例子是，1999 年的火星探测器 Mars Climate Orbiter，就是因为英制单位和公制单位混用而失踪的。

Ada 的答案很简单：

把米和英尺变成不同的类型
混用就变成编译错误
转换要显式写出来

不是靠“小心一点”“靠代码评审抓出来”“靠测试抓出来”，而是从一开始就让它编译不过。

这就是 Ada 的基本态度。

7. 范围约束 —— 在数据类型层面防止非法值

在 Ada 中，类型可以带有数值范围。

subtype Percentage is Integer range 0 .. 100;

Progress : Percentage := 50;

如果试图把超出范围的值放进 Percentage 类型的变量，会在运行期抛出 Constraint_Error 异常。

Progress := 120;  -- 运行期抛出 Constraint_Error

编译期就能判断出的违规，会在编译期被检测出来。

“应该是 0 到 100 之间的值”“应该是 1 以上的值”这类隐含的前提，不用写在注释里，而是能直接用类型表达出来。

事实上，Ada 标准库中也预先定义了一些常用的受约束类型。

Natural  = Integer range 0 .. Integer'Last
Positive = Integer range 1 .. Integer'Last

而且从 Ada 2012 开始，还能给类型附加任意条件作为谓词。

subtype Even is Integer
  with Dynamic_Predicate => Even mod 2 = 0;

像定点数类型这种面向硬件控制的类型，也内置在语言之中。

type Temperature is delta 0.1 range -50.0 .. 150.0;

在很多语言里，非法值的检查往往会变成这样：

在函数开头用 if 语句做校验
漏检查与否全靠代码评审
哪个函数收到的是已校验过的值并不清楚

在 Ada 中，可以说“只要是这个类型的值，范围就已经得到保证”。

校验的责任转移到数据类型上，函数的逻辑就能专注在它本来该做的事上。

8. 数组与下标 —— 边界检查与枚举类型下标

Ada 的数组可以自由选择下标的类型。

type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

type Hours_Array is array (Day) of Natural;

Work_Hours : Hours_Array := (Mon .. Fri => 8, others => 0);

这是以枚举类型 Day 作为下标的数组。

可以用 Work_Hours (Wed) 这样的方式访问，不需要记住“这个数字下标代表什么意思”。

循环也能沿着下标类型来写。

for D in Work_Hours'Range loop
   Put_Line (Day'Image (D) & ":" & Natural'Image (Work_Hours (D)));
end loop;

'Range、'First、'Last、'Length 这类属性，可以随时获取数组的边界信息。

因为不会把边界写死，数组大小的变更不会波及到循环。

而更重要的是，数组访问永远会做边界检查。

Buffer : String (1 .. 10);
Index  : Integer := 11;

Buffer (Index) := 'x';  -- 运行期抛出 Constraint_Error

C/C++ 的缓冲区溢出，多年来一直是安全漏洞的主要原因之一。

在 Ada 中，越界访问不是未定义行为，而是定义明确的异常。

不是悄悄破坏内存、在别的地方引发莫名其妙的崩溃，而是在问题发生的那一刻立刻大声停下来。

考虑到长期运行系统的排查成本，这个差别非常大。

9. 包 —— 规格与实现的分离

Ada 的模块机制是包（package）。

包会分成规格（spec）与实现（body）两个文件。

counters.ads  规格：对外公开的接口
counters.adb  实现：具体细节

规格这样写：

package Counters is

   type Counter is private;

   procedure Increment (C : in out Counter);
   function  Value     (C : Counter) return Natural;

private
   type Counter is record
      Count : Natural := 0;
   end record;

end Counters;

实现这样写：

package body Counters is

   procedure Increment (C : in out Counter) is
   begin
      C.Count := C.Count + 1;
   end Increment;

   function Value (C : Counter) return Natural is
   begin
      return C.Count;
   end Value;

end Counters;

值得注意的地方是：

把 type 声明为 private，调用方就无法碰到内部结构
只要读规格（.ads），就能了解全部的用法
只要规格不变，修改实现（.adb）对调用方来说，需要重新编译的范围就是最小的

这跟 C/C++ 的头文件有点相似，但不是像 #include 那样的文本展开，而是作为语言规格接受一致性检查。

规格与实现不一致，会是编译错误。

此外，参数一定要写出 in、out、in out 这种模式。

procedure Increment (C : in out Counter);

“这个参数只是读、只是写，还是既读又写”，光看签名就能知道。

即使没有指针或引用方面的知识，也能读出数据流动的方向。

10. 记录与判别项

Ada 中相当于结构体的是记录（record）。

type Point is record
   X : Float := 0.0;
   Y : Float := 0.0;
end record;

P : Point := (X => 1.0, Y => 2.0);

字段可以有默认值，也能用具名初始化的聚合（aggregate）来初始化。

很有 Ada 特色的功能是判别项（discriminant）。

type Buffer (Size : Positive) is record
   Data   : String (1 .. Size);
   Length : Natural := 0;
end record;

Small : Buffer (Size => 16);
Large : Buffer (Size => 4096);

判别项是决定记录“形状”的参数。

Buffer (16) 与 Buffer (4096) 是同一个类型，但内部数组的大小在声明时就已经确定，之后不会改变。

大致可以想象成，C 语言里“带有可变长度成员的结构体 + 大小字段”这种模式，被语言以类型的形式安全地管理起来。

大小与实体不一致这种在 C 中常见的 bug 入口，在 Ada 里从一开始就不存在。

11. 泛型

Ada 从 1983 年最初的标准开始，就已经具备泛型（generic）。

这比 C++ 的模板（1990 年代）或 Java 的泛型（2004 年）早得多。

generic
   type Element is private;
procedure Swap (Left, Right : in out Element);

procedure Swap (Left, Right : in out Element) is
   Temp : constant Element := Left;
begin
   Left  := Right;
   Right := Temp;
end Swap;

调用方会用具体的类型来实例化。

procedure Swap_Integers is new Swap (Element => Integer);
procedure Swap_Floats   is new Swap (Element => Float);

Ada 泛型的特点是明确声明所要求的操作。

generic
   type Element is private;
   with function "<" (Left, Right : Element) return Boolean is <>;
function Max (Left, Right : Element) return Element;

规格上会写明“这个泛型函数，要求 Element 类型具备比较运算符”。

C++ 模板长期困扰于“只有实例化之后才知道错误”的问题，在 Ada 中从一开始就不会发生。

C++20 的 concepts 或 Rust 的 trait bound 试图解决的问题，Ada 在 40 年前就已经有了答案。

12. 异常处理

Ada 也有异常处理机制。

with Ada.Text_IO;
with Ada.Exceptions;

procedure Read_Config is
begin
   Load_File ("config.txt");
exception
   when Ada.Text_IO.Name_Error =>
      Ada.Text_IO.Put_Line ("找不到配置文件");
   when E : others =>
      Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (E));
      raise;
end Read_Config;

在代码块的最后写上 exception 部分，按异常种类逐一列出处理逻辑。

语言内置定义的异常，具有代表性的有下面几种：

Constraint_Error  范围约束违规、数组越界、除以零等
Program_Error     违反语言规则（到达不该到达的地方等）
Storage_Error     内存不足
Tasking_Error     任务间通信失败

值得注意的是，范围约束与边界检查的违规，全部都被整合进了这一套异常机制中。

“类型中写下的约束”一旦被打破，就会变成 Constraint_Error。

也就是说，第 7 章看到的范围约束，会作为自动生成的运行期断言发挥作用。

不需要自己动手到处写 if 语句去做检查。

13. 契约式设计 —— 用语言功能写 Pre/Post 条件

Ada 2012 的一大亮点，就是对契约式设计（Design by Contract）的语言级支持。

可以直接在子程序上写前置条件（Pre）与后置条件（Post）。

package Stacks is

   type Stack is private;

   function Is_Full  (S : Stack) return Boolean;
   function Is_Empty (S : Stack) return Boolean;
   function Count    (S : Stack) return Natural;

   procedure Push (S : in out Stack; Item : Integer)
     with Pre  => not Is_Full (S),
          Post => Count (S) = Count (S)'Old + 1;

   procedure Pop (S : in out Stack; Item : out Integer)
     with Pre  => not Is_Empty (S),
          Post => Count (S) = Count (S)'Old - 1;

private
   -- 实现细节
end Stacks;

Pre 是“调用方应该遵守的约定”，Post 是“实现方所保证的约定”。

用 'Old 属性可以引用调用之前的值。

这个契约可以通过编译选项（GNAT 中是 -gnata）启用为运行期检查。

违反契约会抛出 Assertion_Error 异常，可以清楚知道是哪一方违背了约定。

违反 Pre  -> 调用方的 bug
违反 Post -> 实现方的 bug

在文档注释里写“这个函数不能对空栈调用”，跟契约有什么不同呢？

注释和实现走岔了也没人会发现
契约会被编译器检查语法和类型
契约能在运行期自动验证
契约会成为 SPARK 静态证明的输入（第16章）

规格以可验证的形式存在于代码之中。

这就是 Ada 2012 之后的世界。

使用类型不变式（Type_Invariant），还能写出“这个类型的值始终满足这个性质”这样的约束。

14. 任务（Task） —— 并发处理内置于语言之中

Ada 另一个很大的魅力，是并发处理是语言规格的一部分。

C/C++ 让线程依赖操作系统的 API 或库（pthread、std::thread），而 Ada 早在 1983 年，就已经把任务（task）内置在语言之中。

with Ada.Text_IO;

procedure Task_Demo is

   task Worker;

   task body Worker is
   begin
      for I in 1 .. 3 loop
         Ada.Text_IO.Put_Line ("worker:" & Integer'Image (I));
         delay 0.5;
      end loop;
   end Worker;

begin
   for I in 1 .. 3 loop
      Ada.Text_IO.Put_Line ("main  :" & Integer'Image (I));
      delay 0.5;
   end loop;
end Task_Demo;

声明 task 之后，并发执行会在包住它的代码块开始的同一时间启动。

而重要的是，这个代码块要等到内部所有任务都结束才会结束。

“忘了对线程做 join，导致进程结束时发生怪事”这类 bug，在结构上就不会发生。

任务之间的同步，有一个叫做会合（rendezvous）的语言功能。

task Logger is
   entry Write (Message : String);
end Logger;

task body Logger is
begin
   loop
      select
         accept Write (Message : String) do
            Ada.Text_IO.Put_Line (Message);
         end Write;
      or
         terminate;
      end select;
   end loop;
end Logger;

调用方可以用 Logger.Write ("hello"); 这种和过程调用一样的形式来写。

通过消息传递进行任务间通信，完全不需要锁方面的知识就能写出来。

面向实时系统，甚至连调度策略、优先级控制，以及为了便于验证而限制任务功能的 Ravenscar profile 都被标准化了。

15. 保护对象 —— 把互斥控制写成类型

共享数据的互斥控制，会使用 Ada 95 引入的保护对象（protected object）。

protected Shared_Counter is
   procedure Increment;
   function  Value return Natural;
private
   Count : Natural := 0;
end Shared_Counter;

protected body Shared_Counter is

   procedure Increment is
   begin
      Count := Count + 1;
   end Increment;

   function Value return Natural is
   begin
      return Count;
   end Value;

end Shared_Counter;

保护对象的数据，只能通过定义好的操作访问。

而互斥控制则由语言来保证。

procedure  可读写，独占执行
function   只读，允许多个任务同时执行
entry      可以让调用方等到条件（barrier）满足为止

在很多语言里，互斥控制往往只能靠下面这种自觉来维持：

碰这份数据的时候要拿这个互斥锁（mutex）
别忘了释放锁
要遵守锁的获取顺序

在 Ada 的保护对象中，“忘记拿锁的代码”根本就写不出来。

因为数据和保护它的互斥控制，被声明成了同一个类型。

利用 entry 的 barrier 条件，“等到队列里有数据为止”这类条件同步，也不用自己手动管理标志位或条件变量就能写出来。

16. SPARK —— 通往形式化验证之路

在 Ada 的世界里，有一个强大的伙伴叫做 SPARK。

SPARK 是 Ada 的子集（部分语言），设计目的是让程序的性质能被用数学方式证明。

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

SPARK 的工具（GNATprove），可以在不运行的情况下证明这段代码满足下列各项：

不会发生溢出
不会违反范围约束
不会发生除以零
不会读取未初始化的变量
Pre 与 Post 的一致性

它和测试的区别是决定性的。

测试  确认在选定的输入下，程序是否正确运行
证明  证明性质在所有输入下都成立

第 13 章看到的契约（Pre/Post），在 SPARK 中直接成为证明的对象。

原本写成运行期检查的契约，之后可以升级为“已证明”。

SPARK 在航空航天、国防领域积累了实际经验，而近年来 NVIDIA 为了固件安全也采用了它，产业界的应用正在扩大。

“形式化方法太学术，实务上用不上”这种常识，正在被 Ada/SPARK 生态持续、悄悄地推翻。

17. 与 C、C++ 的互操作

Ada 并不是一门孤立的语言。

与 C 的互操作，已经以语言规格（Annex B）的形式标准化。

举例来说，要从 Ada 调用 Windows API 的 Sleep，可以这样写：

with Interfaces.C;

procedure Sleep_Demo is

   procedure Sleep (Milliseconds : Interfaces.C.unsigned)
     with Import,
          Convention    => Stdcall,
          External_Name => "Sleep";

begin
   Sleep (1000);
end Sleep_Demo;

要点如下：

Import           引入外部实现
Convention       指定调用约定（C、Stdcall 等）
External_Name    指定链接时的符号名
Interfaces.C     提供对应 C 类型（int、unsigned、char* 等）的类型

反方向也可以做到。

使用 Export，可以把用 Ada 写的过程公开成能被 C 调用的函数。

也就是说，可以做到下面这种渐进式的用法：

从 Ada 使用现有的 C 库
系统的核心部分只用 Ada/SPARK 写，周边保持 C/C++ 不变
把 Ada 的代码做成 DLL，供其他语言调用

这不是一门“只能整体重写”的语言，而是能与现有资产共存，从重要的部分开始逐步提高可靠性。

18. 开发环境 —— GNAT 与 Alire（在 Windows 上也能跑）

你可能会觉得“想试用 Ada，应该需要昂贵的工具吧”。

但现在，免费就能搭建起相当完整的开发环境。

GNAT         GCC 自带的 Ada 编译器（免费）
Alire        Ada 的包管理工具兼构建工具
GNAT Studio  AdaCore 出品的 IDE
VS Code      装上 Ada Language Server 扩展后，可以用自动补全、跳转定义

特别是 Alire（命令名为 alr）的出现，让 Ada 的入门变得大幅简化。

体验上很接近 Rust 的 cargo。

alr init --bin hello_ada
cd hello_ada
alr build
alr run

用 alr init 创建项目，用 alr build 构建，用 alr run 运行。

工具链（GNAT 本体）也由 Alire 负责获取，因此连手动安装编译器都不需要。

Windows、Linux、macOS 都能运行。

如果你是在 Windows 上开发，下面的流程最快：

1. 从 Alire 官网获取 Windows 版安装程序
2. 用 alr init --bin 创建脚手架
3. 在 VS Code 中装上 Ada 扩展（AdaCore 出品）
4. 用 alr build 构建并运行

库也可以用 alr with 库名 添加。

“因为环境搭建而放弃”的时代已经过去了。

19. Ada 的弱点与注意事项

前面介绍了 Ada 的魅力，但 Ada 也有弱点。

这里公平地整理一下。

生态规模较小
  Web 框架、GUI、云 SDK 等选择比主流语言少
  Alire 的包数量和主流语言差了一个量级

人才和资料较少
  中文资料尤其少
  在团队开发中引入，需要预留学习成本

语法容易让人觉得冗长
  类型声明与规格/实现分离，对小脚本来说显得笨重
  不适合“先跑起来再说”这种用途

招聘市场有限
  偏向航空航天、国防、铁路等领域

而且历史也告诉我们，“用了 Ada 就安全”并不是这么简单的事。

1996 年 Ariane 5 火箭首飞爆炸事故，其原因之一就是用 Ada 写的软件。

把为 Ariane 4 编写的代码，直接复用在飞行特性不同的 Ariane 5 上，结果在转换过程中遇到超出预期范围的大数值，触发了 Constraint_Error，却没有被妥善处理，导致系统停止。

这个事故揭示的是：

语言的运行期检查确实检测到了问题（没有悄悄坏掉）
但运行前提变了却没有被重新验证
异常发生之后的设计（容错机制）并不充分

类型系统和契约，都无法替代重新审视前提假设这一过程。

语言只是安全工程的一部分，不是全部。

我认为，这是学习 Ada 时最诚实的一条提醒。

20. 长生命周期软件与 Ada —— 从维护的角度看

本站经常讨论 Windows 既有资产的维护与延寿问题。

从这个角度来看，Ada 有另一种魅力。

用 Ada 编写的系统，以数十年为单位持续运行的情况并不少见。

而且，Ada 的语言设计本身，就是以长期维护为前提的。

规格（.ads）与实现（.adb）分离
  -> 20 年后的维护者，只要读规格就能掌握接口

强类型与范围约束
  -> 隐含的前提会留在代码里，不用靠口头相传或注释

契约（Pre/Post）
  -> “这个函数的约定”以可验证的形式留存下来

case 的完整性检查
  -> 规格变更时受影响的位置，编译器会帮你列出来

标准修订也重视向后兼容
  -> 大多数 Ada 83 的代码，在现代编译器上依然能通过

这些理念，在用 C# 或 C++ 做长期维护时，也能直接当作设计方针拿来用：

不要用 int，而是定义有意义的类型（表示 ID 的类型、带单位的类型）
把类型设计成无法产生非法值（在构造函数中做校验）
有意识地把公开接口与实现分离
用断言（assertion）或测试来表达前置条件、后置条件
把枚举类型的 switch 写得完整，并把警告当作错误处理

即使工作中没有机会用到 Ada，学习 Ada 的设计理念依然非常有价值。

作为学习“用类型阐述设计”这种感觉的教材，Ada 至今仍是一流的选择。

21. 总结

我们整理了 Ada 的魅力，回顾一下要点：

Ada 是在高可靠性系统中已使用超过 40 年的活跃语言
名字源自 Ada Lovelace，最新标准是 Ada 2022
结构相同但名字不同的类型，是不同的类型。单位混淆会变成编译错误
通过范围约束，可以在类型层面防止非法值
数组会做边界检查，缓冲区溢出不会变成未定义行为
用包分离规格与实现，用参数模式明确标示数据流向
泛型会在规格里写明所要求的操作，因此使用时的错误很明确
Ada 2012 的契约（Pre/Post），能让规格以可验证的形式留在代码中
任务与保护对象，能让并发处理以安全的语言功能来编写
用了 SPARK，就能把契约从运行期检查升级为数学证明
有了 GNAT 与 Alire，免费在 Windows 上就能立刻体验
生态规模小、人才少是它的弱点
语言的安全机制，无法替代重新审视前提假设这一过程

就流行程度而言，Ada 并没有成为主流语言。

但空安全、完整性检查、契约、接近所有权概念的严格性，这些现代语言当作“新功能”引入的东西，Ada 几十年前就已经具备了。

Ada 的本质，可以用一句话概括：

bug 不是用来找出来的，而是靠类型和契约让它“写不出来”的东西。

找个周末，用 Alire 创建一个项目，在被编译器“教育”的过程中试着写一个小程序看看。

当你发现，那一个个编译错误，都是“在变成生产环境事故之前就被抓住的 bug”时，你应该就能体会到 Ada 的魅力所在。

参考资料

• 本文代码片段按章节整理的参考代码集 - komurasoft-blog-samples (GitHub)
• Ada Programming Language - AdaCore
• Learn Ada - AdaCore (learn.adacore.com)
• Introduction to Ada - learn.adacore.com
• Ada Reference Manual (Ada 2022)
• Alire - Ada Library Repository
• GNAT User’s Guide - GCC
• SPARK - AdaCore
• Introduction to SPARK - learn.adacore.com
• Ada Conformity Assessment Authority
• Ariane 501 Inquiry Board Report (ESA)

相关文章

共享相同标签的最新文章。可以围绕相近的主题进一步加深理解。

常见问题

汇总了咨询这一主题时常见的问题。

Ada 语言现在还在使用吗？

是的，而且一直在持续使用。民航飞机的飞行控制、空中交通管制、铁路的信号与联锁系统、火箭与人造卫星、国防系统、医疗设备等，这些一旦出错就会直接关系到人命或造成巨额损失的高可靠性系统中，Ada 已经被使用了数十年。Ada 是一门修订超过 40 年的语言，从 1983 年的 Ada 83 开始，经过 Ada 95、Ada 2005、Ada 2012，最新标准是 Ada 2022。

Ada 语言的强类型和其他语言有什么不同？

在 Ada 中，即使结构完全相同，用不同名字声明的类型也会被当作不同的类型。例如同样用 Float 派生出 Meters 类型和 Seconds 类型，混用时会产生编译错误，转换必须显式写出来。此外，subtype 还能让类型带上数值范围约束（比如 0～100），违反时会在运行期抛出 Constraint_Error 异常。这种设计不是靠“小心一点”去防止单位混淆之类的错误，而是让它“根本编译不过”。

想免费体验 Ada 语言该怎么做？

使用 GNAT（GCC 自带的免费 Ada 编译器）和 Alire（Ada 的包管理工具兼构建工具，命令名为 alr），在 Windows、Linux、macOS 上都能免费搭建完整的开发环境。从 Alire 官网获取安装程序后，用 alr init --bin 创建脚手架项目，alr build 构建，alr run 运行，体验上很接近 Rust 的 cargo。工具链本身也由 Alire 负责获取，所以不需要手动安装编译器。VS Code 也有 AdaCore 出品的 Ada 扩展。

Ada 语言的弱点是什么？

生态规模较小，Web 框架、GUI、云 SDK 等选择比主流语言少；人才和资料（尤其是中文资料）较少，团队引入时需要预留学习成本；类型声明与规格/实现分离对小脚本来说显得笨重；招聘市场也偏向航空航天、国防、铁路等领域。另外，正如 1996 年的 Ariane 5 事故所显示的，语言的安全机制无法替代重新审视前提假设这一过程。

作者简介

本文作者的个人简介页面。

Go Komura

小村软件有限公司 代表

以 Windows 软件开发、技术咨询与故障排查为中心，擅长难以复现的故障调查，以及既有资产仍在运行的项目。