Austral 介绍：一种具有线性类型和 Capabilities 的系统编程语言

Austral 是一种新的系统编程语言。你可以把它看作是 Rust 的精华版，或者是一种现代化、精简的 Ada。它具有强大的静态类型系统、线性类型、基于 Capability 的安全性以及强大的模块化特性。

本文是对该语言的介绍。前几个部分是高层次的，主要介绍该语言的设计理念和思路。接下来的两部分，关于线性类型和基于 Capability 的安全性，则更为详细和技术性，旨在向读者证明关于安全性和正确性的声明是真实的。

目录

1. 设计目标
2. 反特性
3. 特性
4. 语言概述
5. 线性类型
   1. 动机
   2. 什么是线性类型
   3. Universes
   4. Use-Once 规则
   5. 线性类型和安全性
   6. 一个安全的数据库 API
   7. Borrowing
6. 基于 Capability 的安全性
   1. 线性 Capabilities
   2. 一个 Capability 安全的文件系统 API
   3. Root Capability
7. 现状和未来工作
8. 参与其中
9. 结论

设计目标

在 rationale 中有一个章节解释了 Austral 的设计目标，但可以归结为两点：

1. 简单性
2. 严格性

_简单性_对不同的人来说意味着不同的东西。有些人用它来表示熟悉程度、易用性，甚至简洁性。这里的简单性有一个直接的定义：描述一个系统所需的信息量。

复杂的系统，有许多相互影响的移动部件，无法用简短的语言描述。Rube Goldberg 机器、生物学和 C++ 都是复杂的系统。Python 也是一个复杂的系统，尽管它“易于”使用1。简单的系统具有简短的描述。

简单性是一个最重要的目标，因为编程语言_不是工具_。编程语言是工具箱，加上建筑材料，加上产品所在宇宙的物理定律。有时，在极少数情况下，你可以将一个复杂的系统隐藏在一个简单的接口下。但编程语言不是，因为复杂的编程语言就像一个引力常数每天都在变化的宇宙。

有一个著名的 C 语言测验，其中你有一堆看起来很奇怪的程序，必须决定它们的输出是什么。而已经使用该语言多年的人却很难正确回答，因为这些问题指的是 C 规范中微妙而晦涩的特性。

如果你认为弄清楚程序的作用是一个有趣的难题，那么 Austral 就不适合你。语言律师是一种设计缺陷：如果两个人看到同一个基本程序，却对其行为存在分歧，那就是一个问题。

Austral 很简单。规范简短，运行时薄，编译器小。

举一个具体的例子：线性类型系统的设计考虑了极端的简单性。因此，Austral 相当于 borrow checker 的代码少于 600 行，包括 borrowing 和其他符合人体工程学特性的实现。

这里的目标是整个编程语言应该存在于你的脑海中，你应该能够从头到尾阅读规范，并了解关于该语言的所有知识。

_严格性_一半是语言特性，一半是思维方式的转变。

如果飞机像我们编写代码那样飞行，我们每天都会发生坠机事故，当然，除此之外，每次飞机坠毁的反应都会是：“只有糟糕的飞行员才会责怪他们的飞机！如果他们阅读了 C++（呃，737 规范）的第 7.1.5.5 节的第 71 小段，他们就会知道在春分下午 13:51 机翼会掉下来。”

这在航空领域不会发生，因为在航空领域，我们已经正确地决定，人为错误是人类活动固有且不可分割的一部分。因此，我们围绕飞行员构建了同心层的机械制衡，以承担部分飞行负担。因为人类会疲倦、会倦怠、注意力有限、工作记忆有限、因编写可执行的 YAML 而受到创伤，等等。

机械过程——例如类型系统、类型检查、形式验证、契约式设计、静态断言检查、动态断言检查——独立于程序员的技能。机械过程是_可扩展的_，而不是责骂人们少写错误。

严格性很少是一种大的语言特性，而更多的是从其他语言的设计缺陷中学习， “千刀万剐”2，并防止每种缺陷的发生。这可能很难，因为程序员非常依恋这些缺陷。

例如：C 语法中有一个特性，为了简洁起见，你可以编写没有大括号的 if 语句。这引入了一个语法歧义：它被称为“悬挂 else” 问题。有一个关于它的 Wikipedia 文章这一事实应该表明这是不好的。这不是一些抽象的学术问题：它已经导致了现实世界中的安全漏洞。

现在，如果你认为这是一个缺陷，一些程序员会引用旧的终止思考的陈词滥调：“只有糟糕的工匠才会责怪他们的工具！”但这里的权衡是显而易见的：你节省了几个字节和几毫秒的输入时间，但你掷骰子并可能引入一个 CVE，造成数十亿美元的损失。这显然是一个设计缺陷，但如果你建议程序员应该添加大括号，他们会踢踢打打，好像你剥夺了他们的一些基本自由。

Austral 的语法设计考虑了语言安全原则：它是无上下文的，可以从语法中解析，没有“lexer hack”，没有奇怪的、特别的歧义消除机制。语法的语用旨在最大限度地减少混淆和歧义。

例如，考虑运算符优先级问题：任何人都可以记住 PEMDAS，但是编程语言有许多种类的二元运算符——算术、比较、按位、布尔——将它们混合在一起会产生错误的余地（x ^ y && z / w 的计算结果是什么？）。因此，在 Austral 中，根本没有运算符优先级：任何深度大于一级的二元表达式都完全加上括号。你必须输入更多，但我们不是打字员，我们是程序员，我们的任务是_向他人_传达我们希望计算机做什么。如有疑问：通过简化语言来简化。

这并不适合所有人。但这适合我，因为在行业工作了十年之后，我从编程语言中最不想得到的就是“力量”。我想要的是更少的噩梦。编程语言提供的“自由”感觉像是表达能力_直到_你的代码库成为一个精神健康超级基金站点。

反特性

在介绍语言特性之前，我想列出_反特性_。以下是 Austral 自豪地没有的东西：

1. 没有普遍存在的 NULL，因此也没有空指针解引用错误。你必须使用显式的 Option 类型。
2. 没有垃圾收集，因此运行时可以很薄并且性能是可预测的。
3. 没有异常，没有堆栈展开，也没有析构函数。
4. 没有意外的控制流：你有条件语句、循环和函数调用。没有别的了。
5. 任何地方都没有隐式类型转换。
6. 更一般地说：没有隐式函数调用。如果它不在源代码中，它就不会发生，你也不会为此付出代价。
7. 没有全局状态。
8. 没有运行时反射。
9. 没有宏。
10. 没有 Java 或 Python 风格的 @Annotations。
11. 没有类型推断：类型信息仅沿一个方向流动，函数参数、局部变量、_等等_必须注释其类型。
12. 没有一流的 async3。
13. 函数重载通过 typeclass 受到很大限制（想想 C++ concepts）。并且基本的算术运算符不能重载4。
14. 没有语法歧义：没有 dangling else（因此，也没有 gotofail)，没有算术优先级，没有任何种类的语法优先级规则。
15. 没有语法扩展：例如，你不能引入新的中缀运算符。

特性

Austral _拥有_什么：

1. 一个强大、静态的类型系统，不太过于聪明。
2. 一个类型系统，允许正确且安全地处理资源，而没有运行时开销。“资源”在这里意味着内存和任何具有显式创建-使用-销毁生命周期的东西：文件句柄、套接字、数据库句柄。
3. 基于 Capability 的安全性，可防止供应链攻击。你的 left-pad 依赖项不会被破坏，无法将你磁盘的内容上传到远程服务器。这是因为执行网络访问的代码必须显式地获得网络 Capability，执行文件系统访问的代码需要文件系统 Capability，等等。一个声称需要网络访问的字符串填充函数会立即脱颖而出。Capabilities 是代码的不可伪造的安全授权令牌。
4. 一个强大的、受 Ada 启发的模块系统，它不与文件系统结构相关联，并将模块接口与实现分离。
5. Sum types 带有模式匹配和穷举检查。
6. Type classes，如在 Haskell 中一样，用于限制函数重载。与 Haskell 中一样，类型参数可以被约束为仅接受实现给定 typeclass 的类型。
7. 一个严格的、无上下文的、明确的语法，受 langsec 思想的启发。

语言概述

最大的代码组织单位是模块。模块具有显式名称，并且与文件系统分离，如 Haskell 和 Python 不同。模块分为接口和实现，如 Ada 或 OCaml。

这_不是_，如在 C 或 C++ 中一样，是一种启用单独编译的 hack。这是关于可读性和关注点分离。接口文件包含公共声明，但不包含代码。实现文件包含接口文件中内容的实现，以及私有声明。

有五种声明：

1. 常量。
2. 类型。
3. 函数。
4. Type classes。
5. Type class 实例。

每种声明都可以是公共的（通过出现在接口文件中）或私有的，这决定了它们是否可以被其他模块导入。类型具有额外的可见性状态：opaque，这意味着它们可以被其他模块导入，但它们不能在模块外部构造或访问其内容，除非通过模块的公共 API。Opaque 类型是隐藏其内部的数据结构的明显选择。

函数的工作方式符合你的预期：它们接受值并返回它们。没有 void，而是一个具有名为 nil 的常量的 Unit 类型。

Type classes 定义了类型可以符合的接口，而实例定义了特定类型如何实现特定 typeclass。

类型和函数可以是泛型的。泛型的工作方式与大多数语言略有不同，因为有线性系统。

线性类型

很难宣传一种语言是“简单”的，然后开始谈论“线性类型”和“类型 universes”，但只有这些词是新的。这些概念很简单。Austral 的整个线性类型系统可以放在一页纸上。因此，这不是一些抽象的象牙塔特性，你需要拥有范畴论博士学位才能理解。

线性类型使我们能够进行手动内存管理，而没有运行时开销，也没有安全漏洞：它们可以防止内存泄漏、use-after-free 和 double-free 错误。

这不仅限于内存，还扩展到任何具有生命周期的东西，我们必须以一定的顺序创建它、使用它和销毁它。文件句柄、网络套接字、数据库句柄、锁和互斥锁：这些对象的正确使用可以在编译时强制执行。

首先，我将解释动机：为什么我们需要线性类型？然后我将解释它们是什么，以及它们如何提供安全性。

动机

考虑一个文件处理 API：

type File
File openFile(String path)
File writeString(File file, String content)
void closeFile(File file)

一位经验丰富的程序员理解 File 对象的_隐式生命周期_：

1. 我们通过调用 openFile 创建一个 File 句柄。
2. 我们向句柄写入零次或多次。
3. 我们通过调用 closeFile 关闭文件句柄。

我们可以用图形方式将其描述为：

但至关重要的是：此生命周期_不是由编译器强制执行的_。我们不考虑许多错误的转换，但这些转换在技术上是可能的：

这些错误分为两类：

1. 泄漏： 我们可以忘记调用 closeFile，例如：

 let file = openFile("hello.txt");
 writeString(file, "Hello, world!");
 // 忘记关闭

2. Use-After-Close： 我们可以对已经关闭的 File 对象调用 writeString：

closeFile(file);
writeString(file, "Goodbye, world!");

我们可以在关闭文件句柄后再次关闭它：

closeFile(file);
closeFile(file);

在一个像这样的短线性程序中，我们不太可能犯这些错误。但是，当句柄存储在数据结构中并四处移动，并且生命周期调用在时间和空间上分离时，这些错误变得更加常见。

它们不仅适用于文件。考虑一个数据库访问 API：

type Db
Db connect(String host)
Rows query(Db db, String query)
void close(Db db)

同样：在调用 close 之后，我们仍然可以调用 query 和 close。我们也可以完全忘记调用 close。

而且——至关重要的是——考虑这个内存管理 API：

type Pointer<T>
Pointer<T> allocate(T value)
T load(Pointer<T> ptr)
void store(Pointer<T> ptr, T value)
void free(Pointer<T> ptr)

在这里，同样，我们可以忘记在分配指针后调用 free，我们可以在同一个指针上调用 free 两次，并且更糟糕的是，我们可以在已释放的指针上调用 load 和 store。

无论我们在哪里有_资源_ ——具有关联生命周期的类型，必须按顺序创建、使用和销毁——我们都有相同类型的错误：忘记销毁一个值，或者在使用一个值之后销毁它。

在内存管理的上下文中，指针生命周期错误非常灾难性，它们有自己的名称：

1. Double free errors。
2. Use-after-free errors。

当然，计算机科学家们已经尝试解决这些问题。传统的方法称为_静态分析_：一群博士会编写一个程序，该程序会遍历源代码并执行各种检查，并找到可能发生这些错误的地方。

关于使用静态分析来捕获这些错误的大量论文、会议记录、大学幻灯片等已经被撰写。但是静态分析的问题有三重：

1. 这是一个移动目标。虽然类型系统是相对固定的——即，类型检查规则在语言版本中是相同的——但静态分析器往往会随着每个版本而变化，因此在软件的每个较新版本中，你都会获得越来越复杂的启发式方法。
2. 与单元测试一样，它通常可以显示错误的_存在_，但不能显示错误的_缺失_。可能存在误报——代码完全没问题，但静态分析器将其标记为不正确——但更危险的是漏报，即静态分析器返回对具有漏洞的代码的全部清除。
3. 静态分析是不透明的启发式堆。因为分析总是在变化，所以不期望程序员开发静态分析器的心理模型，并牢记该模型编写代码。相反，他们应该编写他们通常编写的代码，然后将静态分析器扔给它并希望最好。

我们想要的是一种解决这些问题的方法，该方法是_静态_和_完整_的。静态的，因为它是一组固定的规则，你可以学习一次并记住，就像类型系统的工作方式一样。完整的，因为它_没有漏报_，并且捕获_每个_生命周期错误。

最重要的是：我们希望它很简单，这样处理它的程序员可以完全理解它。

因此，总结我们的要求：

1. 正确性要求： 我们希望确保资源以正确的生命周期使用。
2. 简单性要求： 我们希望该机制很简单，也就是说，程序员应该能够将它保存在脑海中。这排除了涉及定理证明、SMT 求解器、符号执行等复杂解决方案。
3. 静态性要求： 我们希望它是一组固定的规则，而不是一个不断增长、不断变化的启发式堆。

所有这些目标都是可以实现的：解决方案是_线性类型_。

什么是线性类型

在物理世界中，一个物体占据空间中的一个点，物体可以从一个地方移动到另一个地方。但是，复制一个物体是不可能的。计算机颠倒了这一点：复制是原始操作。虽然内存中的一个对象驻留在单个位置，但是对该对象的_引用_或指针可以被复制多次，并通过线程传递，并且这种疯狂复制东西的自由是所有与资源相关的安全漏洞的根源。

_类型_是一组共享某些结构的值。_线性类型_是一种其值只能使用一次的类型。

线性值的工作方式类似于真实世界的对象：它们占据空间中的一个点，并且可以传递，但_不能复制_。这种限制听起来可能很麻烦（并且与问题无关），但我们将看到事实并非如此。

Austral 的线性类型系统仅由两条规则定义：线性 Universe 规则和 Use-Once 规则。

Universes

首先，类型集分为两个 universes：free universe，包含可以无限次使用的类型（例如布尔值、机器大小的整数、浮点数、包含 free 类型的记录等）；以及 linear universe，包含线性类型，通常代表资源（指针、文件句柄、数据库句柄等）。

类型通过以下两种方式之一进入线性 universe：

第一种是通过 fiat：一个类型可以简单地声明为线性的，即使它只包含 free 类型。稍后我们将看到为什么这很有用。

-- `Pos` 被声明为线性的，即使它
-- 只包含 free 类型。
record Pos: Linear is
  x: Int32;
  y: Int32;
end;

第二种是通过包含：线性类型可以被认为是“病毒式的”。如果一个类型包含一个线性类型的值，它会自动变为线性的。

因此，如果你有一个线性类型 T，那么像这样的记录：

record Example: Linear is
  a: A;
  b: B;
  c: Pair[T, A];
end;

是线性的，因为字段 c 包含一个类型，该类型又包含 T。其中一个变体包含线性类型的 union 或 enum，毫不奇怪，也是线性的。你不能偷偷地将线性类型放入 free 类型中。

线性类型的病毒性确保你不会意外地逃脱线性。

Use-Once 规则

线性类型的值必须使用一次且仅使用一次。不是_可以_：必须。它不能使用零次。这可以通过一组非常简单的检查完全在编译时强制执行。

要理解“使用”线性值意味着什么，让我们看一些例子。

假设你有一个函数 f，它返回一个线性类型 L 的值。

那么，以下代码：

begin
  let x: L := f();
end;

是不正确的。x 是一个线性类型的变量，它被使用了零次。编译器会抱怨 x 被静默丢弃。

类似地，如果你有：

begin
  f();
end;

编译器会抱怨 f 的返回值被静默丢弃，你不能对线性类型执行此操作。

如果你有：

begin
  let x: L := f();
  g(x);
  h(x);
end;

编译器会抱怨 x 被使用了两次：它被传递给 g，此时据说它被_消耗了_，但随后它被传递给 h，这是不允许的。

但是，以下代码通过：x 被使用了一次且仅一次：

begin
  let x: L := f();
  g(x);
end;

然而，“使用”并不意味着“在代码中出现一次”。考虑 if 语句如何工作。编译器会抱怨以下代码，因为即使 x 在源代码中仅出现一次，它也没有被“使用一次”，而是被使用——我该怎么说呢？0.5 次？：

begin
  let x: L := f();
  if cond() then
    g(x);
  else
    -- 什么都不做。
    skip;
  end if;
end;

变量 x 在一个分支中被消耗，但在另一个分支中没有被消耗，编译器不满意。如果我们将代码更改为：

begin
  let x: L := f();
  if cond() then
    g(x);
  else
    h(x);
  end if;
end;

那么我们就没事了。这里的规则是，在线性类型中，在 if 语句之外定义的变量，必须在该语句中使用零次，或者在每个分支中使用一次。

类似的限制适用于循环。我们不能这样做：

begin
  let x: L := f();
  while cond() do
    g(x);
  end while;
end;

因为即使 x 出现一次，它也被_使用_了多次：它在每次迭代中使用一次。此处的规则是，在线性类型中，在循环外部定义的变量不能出现在循环体中。

就是这样。就是这样。我们有一组固定的规则，它们非常简短，你可以在几分钟内学会它们。因此，我们满足了上一节中列出的简单性和静态性要求。

但是线性类型是否满足正确性要求？在下一节中，我们将看到线性类型如何使强制值应按照生命周期使用成为可能。

线性类型和安全性

让我们考虑一个线性文件系统 API。我们将使用 Austral 模块规范的语法：

module Files is
  type File : Linear;
  function openFile(path: String): File;
  function writeString(file: File, content: String): File;
  function closeFile(file: File): Unit;
end module.

openFile 函数非常正常：接受一个路径并返回一个线性 File 对象。

writeString 是不同的地方：它接受一个线性 File 对象（并消耗它）和一个字符串，并返回一个“新”的线性 File 对象。“新”是带引号的，因为它只是从类型系统的角度来看是一个新的线性值：它仍然是同一个文件的句柄。但是不要过多地考虑实现：稍后我们将研究如何实现这一点。

closeFile 是 File 类型的析构函数，并且是生命周期图的终点：File 进入并且不离开，并且该对象被处理掉。让我们看看线性类型如何帮助我们编写安全代码。

我们可以泄漏 File 对象吗？不能：

let file: File := openFile("test.txt");
-- 什么都不做。

编译器会抱怨：变量 file 被使用了零次。或者：

let file: File := openFile("test.txt");
writeString(file, "Hello, world!");

writeString 的返回值是一个线性 File 对象，它被静默丢弃。编译器会向我们抱怨。

我们可以从生命周期图中删除“泄漏”转换：

我们可以关闭文件两次吗？不能：

let file: File := openFile("test.txt");
closeFile(file);
closeFile(file);

编译器会抱怨你试图消耗一个线性变量两次。所以我们可以从生命周期图中删除“double close”错误转换：

你可以看到这是要去哪里。我们可以在关闭文件后写入文件吗？不能：

let file: File := openFile("test.txt");
closeFile(file);
let file2: File := writeString(file, "Doing some mischief.");

编译器会再次抱怨我们消耗了 file 两次。因此，我们可以从生命周期图中删除“use after close”转换：

我们已经完成了一个完整的循环：编译器强制执行的生命周期与我们预期的生命周期完全一对一。

最终，只有一种使用此 API 的方法不会让编译器抱怨：

let f: File := openFile("test.txt");
let f1: File := writeString(f, "First line");
let f2: File := writeString(f1, "Another line");
...
let f15: File := writeString(f14, "Last line");
closeFile(f15);

请注意文件值是如何“线程化”到代码中的，以及每个线性变量是如何只使用一次的。

现在，我们在上一节中概述的要求中获得了三比三的成绩：

1. 正确性要求： 它正确吗？是的：线性类型允许我们定义 API，以便编译器完美地强制执行生命周期。
2. 简单性要求： 它简单吗？是的：类型系统规则可以放在餐巾纸上。无需使用 SMT 求解器、证明关于代码的定理，或进行符号执行并探索程序的状态空间。线性检查很简单：我们遍历代码并计算变量出现的次数，注意正确处理循环和 if 语句。我们还确保线性值不能被静默丢弃。
3. 静态性要求： 这是一个不断增长、不断变化的启发式堆吗？不：它是一组固定的规则。学一次，用一辈子。

一个安全的数据库 API

这个解决方案是否通用？让我们考虑一个线性数据库 API：

module Database is
  type Db: Linear;
  function connect(host: String): Db;
  function query(db: Db, query: String): Pair[Db, Rows];
  function close(db: Db): Unit;
end module.

这一个稍微复杂一些：query 函数必须返回一个元组，其中包含新的 Db 句柄和结果集。

同样：我们不能泄漏数据库句柄：

let db: Db := connect("localhost");
-- 什么都不做。

因为编译器会指出 db 从未被消耗。我们不能 close 数据库句柄两次：

let db: Db := connect("localhost");
close(db);
close(db); -- 错误：`db` 再次被消耗。

因为 db 被使用了两次。类似地，我们不能在关闭数据库后查询数据库：

let db: Db := connect("localhost");
close(db);
-- 下面是元组解构符号。
let { first as db1: Db, second: Rows } := query(db, "SELECT ...");
close(db); -- 错误：`db` 再次被消耗。
-- 另一个错误：`db1` 从未被消耗。

原因相同。正确使用数据库的唯一方法是：

let db: Db := connect("localhost");
let { first as db1: Db, second: Rows } = query(db, "SELECT ...");
// 迭代行或类似操作。
close(db1);

Borrowing

从每个函数返回元组并将线性值线程化到代码中非常冗长。

这也常常违反最小特权原则：线性值在某种意义上具有“根权限”。如果你有一个线性值，你可以销毁它。考虑上面描述的线性指针 API：load 函数可以在内部取消分配指针并再次分配它。

我们不会_期望_会发生这种情况，但重点是要具有防御性。我们希望语言为我们提供一些保证：如果一个函数应该只能从线性值读取数据，但不能取消分配它或改变其内部，我们希望有一种方法来表示这一点。

Borrowing 是从 Rust 那里偷来的。它通过允许我们在限定的上下文中将线性值视为 Free 来提高人体工程学。它允许我们降低权限：应该只能从线性值读取数据的函数可以采用只读引用，应该能够改变（但不能销毁）线性值的函数可以采用可变引用。

传递线性值本身是最高级别的权限：它允许接收函数对该值执行任何操作，从而完全拥有该值。

与 Rust 不同，Austral 的 borrowing 受到更多限制。权衡是：你必须输入更多，但是区域生命周期在语法上更清晰，并且模型在概念上更简单。这就是线性检查器只有 600 行 OCaml 代码的原因。

基于 Capability 的安全性

如果你阅读 80 年代的软件工程文献，那么最令人担忧的是软件重用。今天，我们面临相反的问题：包生态系统包含数十万个由许多作者编写的包，并且应用程序可传递地具有数千个依赖项。这引入了一类新的安全漏洞：供应链攻击，攻击者会将恶意软件添加到数百万台计算机可传递使用的单个库中。

但是，为什么成千上万个恶意软件依赖项中的_单个_依赖项足以危害安全性？因为代码在很大程度上是无权限的。或者更确切地说：所有代码都具有相同的权限级别：做任何事情。如果不检查代码，你将无法知道 leftPad 是填充字符串_还是_读取你的整个主目录并将其上传到远程服务器。

Austral 的解决方案是基于 Capability 的安全性。代码应该被授权。要访问文件系统、网络或其他特权资源，库应要求获得这样做的权限。然后，从函数签名中可以明显看出每个