4. 数学视角的操作系统 🌶️

操作系统就是直接运行在计算机硬件上的程序，它提供了应用程序执行的支撑和一组 API (系统调用)：操作系统内核被加载后，拥有完整计算机的控制权限，包括中断和 I/O 设备，因此可以构造出多个应用程序同时执行的 “假象”。

本讲内容 (科普性质)：一个 “模拟” 的操作系统模型。

4.1 数学视角的计算机程序

计算机辅助证明并不是一个新概念：我们不再用自然语言，而是用严格的、机器可检查的逻辑语言书写证明，核心技术是揭示了数学证明与类型系统之间的深刻联系的 Curry-Howard Correspondence：

1. 命题即类型：逻辑中的命题 (如 $A \to B$) 对应函数类型 $A \to B$。
2. 证明即程序：命题的构造性证明过程对应该类型的一个具体程序（例如，一个实现 $A \to B$ 的函数即为 “$A$ 蕴含 $B$” 的证明）。

逻辑中的蕴含消除规则对应函数调用：若有一个类型为 $A\to B$ 的函数 (证明)，且输入类型 $A$ 的值 (前提)，则输出类型 $B$ 的值 (结论)。而对于一阶谓词，例如 $\exists x. P(x)$，就必须提供一个 $x$ 的实例，这构成了基于构造的 “直觉逻辑” 的基础。

Proof assistant 是人工智能时代堪称完美的辅助工具：如果我们要信任 AI 产生的结果，就让它们给出一个 proof assistant 认可的证明吧！延伸阅读：科普文章: “Formal verification doesn’t result in perfect code; it simply narrows the possibility for errors and vulnerabilities to creep in,” Parno says. “What makes the technique so attractive is that you push the uncertainty or scope of problems down to smaller and smaller windows”

4.2 数学视角的操作系统

4.3 状态机模型与模型检查器

下面是我们绘制一个 “Hello World” 状态空间的例子。Hello 会调用一个有趣的系统调用 fork，它的行为是复制状态机的当前状态：

我们将会在这个学期里，同时分析模型和真实操作系统 (Linux) 系统调用的行为，帮助大家在概念 (抽象) 和具体 (实现) 层面理解操作系统。

4.4 总结

Take-away Messages: 程序就是状态机；状态机可以用程序表示。因此：我们可以用更 “简单” 的方式 (例如 Python) 描述状态机、建模操作系统上的应用，并且实现操作系统的可执行模型。而一旦把操作系统、应用程序当做 “数学对象” 处理，那么我们图论、数理逻辑中的工具就能被应用于处理程序，甚至可以用图遍历的方法证明程序的正确性。