Antithesis杰出工程师Sean Allen：穷举匹配让遗漏分支变成编译错误，比测试更早捕获缺陷

Sean Allen是Antithesis的杰出工程师，也是面向并发的编程语言Pony的核心贡献者，此前在微软从事机密计算工作。他在与The Pragmatic Engineer的访谈中提出了一个反直觉的立场：对于真正关心正确性的工程师来说，测试是优先级最低的手段。

他的核心论点是：测试发生在开发流程的晚期，而你应该在到达测试之前尽可能多地完成验证。具体来说，ML系语言（Standard ML、OCaml、F#，以及受其影响的Rust）提供的类型系统可以在编译期捕获大量错误。他举了一个关键机制：当你有一个包含五种情况的和类型（sum type），使用穷举模式匹配时，如果你把它扩展到六种，编译器会立刻告诉你代码库中每一个没有处理第六种情况的位置。穷举匹配把每一个「忘记处理新分支」的bug变成了编译错误。

这背后的原则是「让非法状态不可表达」。类型系统能表达状态和合法转换，一旦这些就位，系统就不可能进入你不期望的状态。你只需要测试类型系统无法表达的那部分逻辑，而不是整个系统。

Allen进一步区分了测试和负载（workload）。他认为，对分布式系统或数据库做属性测试时，真正有效的不是随机生成输入，而是定义一个负载：输入是你驱动代码的操作（如GET、PUT、DELETE），验证是你用来确认系统正常工作的规则。他举了Bank Test作为具体例子：系统中有一万美元分在十个账户，负载不断在账户间转账，同时一个检查组件持续查询总额。如果隔离保证成立，它应该永远只看到一万美元。这个负载不需要指定转多少、何时转，它只描述转账如何发生，然后让不变量自己暴露问题。

他承认这个方法的边界：在小系统中，如果你能把一切装进脑子里，确实可以不太依赖编译器。但当系统变大、团队变多，删除一个类后编译器能告诉你所有会坏的地方，这种能力就变得不可替代。

Gergely在访谈前言中提到，他正越来越关注软件正确性——AI代理产出的代码量前所未有，这意味着更多缺陷有机会被部署到生产环境。Sean的立场——在测试之前就通过类型系统和负载验证捕获问题——恰好回应了这一关切。