结构正确性

# 结构正确性 — sao.dev 来源：https://blog.sao.dev/structural-correctness/ 类型系统很棒：它们在编译时捕获大量 bug，并为应用的后续开发贡献了语法/词汇。与类型系统类似，现代的正确性验证工具通过基于图结构的问题域模型，利用**结构性描述**来工作： - **类型系统**将程序描述为类型、函数、trait/等的图，及其相互关系。类型是节点，关系（如 `返回`、`接受`、`实现`等）是边。 - **构建系统**（如 Bazel）以构建目标为节点，以依赖关系为节点间的边。如果没有显式声明依赖，未声明的包即使通过其他方式被构建，也不会提供给构建目标，从而实现了封闭性和简单的可部署性。 - **接口描述语言**将消息类型和服务作为节点，返回值类型和参数类型作为边（一种受限的类型系统）。 - **数据库**使用外键（边）来描述相关表行（节点）之间的关系。然而，数据库也使用检查约束来实现正确性：这些不是结构性的，但作为有用的谓词，可以表达无法通过附加方式描述的方面。 将你的领域建模为类型化节点和边的图。这些图中最优秀的是定义性的：描述系统的结构*就是*系统本身。没有边，就没有能力。 每个领域都有自己的节点和边类型词汇表。Bazel 是通过不同边类型展现丰富性的一个好例子：deps 表示“链接此代码”，srcs 表示“编译这些文件”，data 表示“在运行时可用”。每种都是目标图中的不同边类型，每种都构成不同的能力。优雅地选择节点和边类型会带来表现力强且功能强大的工具。许多这些正确性工具同时利用结构正确性和谓词来描述有效配置。 这些基于图结构的系统中最好的那些是构成性/定义性的：它们既定义了“什么是有效的”，也定义了“输出如何计算”。在 Bazel 中，目标不能导入它没有 `dep` 依赖的模块。这提供了两个有价值的特性：a) 必须声明可验证的不变量系统才能运行，因此你默认得到的是一个可验证的系统；b) 由于声明的属性和关系同时服务于行为和验证，这带来了规格说明的简洁性。构建一个 Bazel 项目迫使你描述产品的显式结构，并让你在继续开发时拥有验证它的手段。 关于“每个领域都有自己的名词和动词”以及“定义性的图结构系统”这两点，正是 Bazel 成为描述整个产品良好基础的原因：Bazel 允许你为领域概念（包、服务、数据集）定义任意的节点类型，通过类型化的边约束它们之间的关系，然后从这一单一的结构描述中派生出整个构建/测试/部署流水线。一个服务、它的指标端点以及抓取它的 Prometheus 部署都可以成为同一个图中的节点——它们的关系声明一次，用于编译、部署和验证整个系统。 ## 那么状态呢？ 很高兴你问到！数据库通过模式定义的表、外键和检查约束来定义可以存储什么。但除此之外，它们并不指定有效的状态转换。这通常留给应用层，依赖 HTTP 或 RPC 端点来忠实地实现业务逻辑。然而，这常常是出错的地方：例如，两个端点都修改订单状态，其中一个在将其标记为 `已发货` 之前忘记了检查库存。 着色Petri网（CPN）在模式定义的集合（库所/令牌 (https://cpn.sao.dev/concepts/places-and-tokens)）基础上，通过变迁 (https://cpn.sao.dev/concepts/transitions) 添加了严格的“下一状态”定义。在 CPN 中，状态只能通过选择特定的绑定 (https://cpn.sao.dev/concepts/bindings) 并触发其变迁来改变，消耗、改变、产生特定库所中的令牌。这是图结构系统在状态上的应用：库所和变迁是节点，连接它们的弧是边。与 Bazel 类似，定义 CPN 系统功能的概念同时也更完整地用于验证该系统的手段。 为了演示 CPN 如何做到这一点，让我们来看一个相当复杂的例子：一个网页爬虫。我在原始的CPN文章 (https://blog.sao.dev/cpns-llms-distributed-apps/) 中将我描述的那个网页爬虫实现为一个感兴趣的应用。在这个例子中，爬虫需要使用一组轮换的代理，并实现对域的“租赁”语义，以防止站点过载等。传统上，构建这样一个有状态系统意味着协调分散在多个层中：数据库处理资源状态（通过 `SELECT FOR UPDATE` 和谨慎的锁排序），任务队列处理作业调度，应用代码处理速率限制和冷却逻辑，另一个组件则强制执行域并发限制。每个组件都有自己的不完整正确性视图。你通过编写检查约束、单元测试和应用级谓词来增加可靠性，并通过反复试验确保它们一致。 > 代理的守恒不是你要测试的属性，而是网络的拓扑事实。 使用 CPN，爬虫的整个协调模型被声明为令牌和变迁。声明一个用于爬取的资源是一个单一的变迁（`select_resource`），它在可用资源、代理和域状态之间进行绑定。它在同一次触发中原子性地租用一个代理，增加域的活跃计数，并创建一个会话。没有需要搞对的锁定策略，因为绑定系统保证只参与有效的组合。代理的守恒不是你要测试的属性，因为这是一个拓扑事实：一个代理令牌在任何时刻都恰好存在于一个库所（`available_proxies` 或 `leased_proxies`）中，并且只有声明的变迁才能移动它。资源生命周期（`available` → `leased` → `cooling` → `available`）就是网络本身的形状，实际上是一个状态机。 此外，它还为你提供了一个很酷的网络动画来展示： 全尺寸 (https://viz.cpn.sao.dev/scraper/)——网页爬虫 CPN，动画版 就我个人而言，我对这种状态与变迁的统一感到乐观：数据库通常只处理数据 + 类型这一面，再加上诸如检查约束之类的谓词工具。现有系统将状态相关的不变量分散在应用代码、单元测试和数据库约束中（各自有独立的验证），而 CPN 统一了这些关注点，并用它们来定义应用功能。 作为一个新领域，前路还有很多需要学习：这些系统可能出现什么样的 bug，需要做出什么样的操作和性能权衡。类型系统并非免费是众所周知的事情。但我看到随之而来的机遇甚至更大。