你以为AI生成代码更需数学证明？形式化方法专家：可能正好相反

“我正在加载一个视频。出于某种原因，它的感觉——它的加载速度——比其他东西慢。”这是在The Pragmatic Engineer播客最新一期节目中，主持人Gergely Orosz演示一个开源项目时的随口一说。他点开的是Hillel Wayne笔下的一个文件，只看见寥寥数行代码。Gergely的反应很本能：“等一下，只有45行代码？才这么点儿？”

屏幕那头的Hillel Wayne只是轻声回应了一句：“是的。就是这些。”这位形式化方法顾问、教育者和作家，正在用最朴素的方式，向你展示软件工程中被大多数人遗忘的一个角落。在这个动辄数万行代码、数十个微服务交互的时代，真正的核心规约，有时只需要45行就能锁定整个系统的行为边界。这不是反直觉，而是反常识。

很多人有一个美妙的设想：当人工智能开始生成大部分甚至所有代码，人类对数学证明式的绝对正确性需求会爆发式增长，于是形式化方法会自然走向主流。Hillel Wayne显然对这套逻辑有自己的判断。在Gergely的追问下，他坐在自己的书架前，语气并不激动，但毫不含糊地表达了自己的怀疑。他甚至不认为这是一个“AI将改变一切”的简单故事——反而，事情的走向可能与这份乐观的预测截然相反。

✏️ 我们算不算是“真正的工程师”？

在深入AI和形式化验证之前，Gergely先抛出了一个身份问题：软件工程师到底算不算“工程师”？这个争论存在了二十年。反对者常拿土木工程、机械工程的精确性来对比软件的脆弱与不确定性，支持者则强调我们处理的复杂度有过之而无不及。

为了给出一个经得起推敲的答案，Hillel做了一个名为The Crossover Project的深度研究。他采访了大约20位分别来自传统工程领域和软件工程领域的从业者。研究的结果并不支持那种非黑即白的论断。他发现，两者之间既有显著的相似性，也有深刻的差异。最终的结论是：软件开发过程所需的那份严谨性，足够我们赢得“工程师”这个称号。

但在交叉研究中，他发现了一个让传统工程师无比艳羡的存在：Git。在其他工程领域，变更管理向来是一笔糊涂账。机械工程师修改图纸、土木工程师调整结构方案，都有一套自己的控制流程，但没有任何工具能像软件工程里的Git那样，超越式地提供分支、回滚、原子化提交和代码审查能力。Hillel的原话是：“传统工程师非常希望他们的领域也有版本控制这个概念，因为它要复杂和先进得多。”这不只是一个工具的差距，而是工作哲学的差异。

45行代码如何描述整个世界

现在话题可以拉回播客开头那个时刻了。那个被Gergely惊叹“只有45行”的文件，是用TLA+写就的一份形式规约。TLA+，全称Temporal Logic of Actions，是由数学家Leslie Lamport发明的一种形式化规约语言。如果你对这个名字有印象，那是因为他也是LaTeX的创造者。

Lamport设计TLA+的初衷，是想抛开具体的代码实现细节，只做一件事：为复杂系统建模。你不需要关心网络包怎么收发，锁怎么获取，只需要定义系统的所有合法状态，以及状态之间允许的流转路径。在Hillel的现场演示里，一个系统被抽象为状态机。从一个起始状态出发，TLA+的工具链会穷举每一个可达的状态，然后逐一核对：你在规约里提前写好的那些不变式，在所有这些状态下是否还站立得住？

这种思维方式与程序员日常的编码习惯几乎是逆向的。我们习惯了“我跑几个测试用例看看对不对”，而TLA+的哲学是：“我不跑测试，我跑的是所有可能的历史。”任何一个你漏掉的、测试根本没想到要去覆盖的并发路径，在TLA+的模型检查器眼里都无所遁形。它不测试一个实现，它检查一个设计。

Amazon与那个“几乎不可能发现”的bug

如果你觉得这依然像学术界的自娱自乐，那么不妨看看Amazon的工程实践。在播客的对话中，Hillel引述了一个只有一线工程师才可能留下的技术记忆。Amazon曾经在一个核心分布式系统的设计阶段，使用TLA+找到了一个隐藏极深的缺陷。

这个bug的狡猾之处在于，它大概率不会被传统的测试方法抓到。单元测试探测不到，因为单个组件单独跑的时候逻辑完美。集成测试也难，因为你需要极其精巧的并发时序才能触发那个状态冲突。压力测试更没用，它只会把你导向常规的性能瓶颈，而非一个路径空间的死角。最终，是TLA+在穷举状态空间时，捕获了那条通往灾难的窄路。Hillel在节目里对这个案例的定性是：“一个用其他方式几乎不可能定位到的bug。”

这件事的冲击力在于，它验证了一个残酷的现实：在分布式系统面前，人类的并发直觉是系统性地靠不住的。我们的脑子本能地思考线性故事——先A后B，然后C。但分布式系统不按故事线运行，它按交错的历史运行。而TLA+的意义，就是把所有这些交错的历史，一次性铺开在你眼前。

设计当先，修补其次

在Hillel的工作流里，TLA+从来不负责检查你写好的代码是否准确。它切入的环节更早：在你动手写Go、Rust或者Python的第一行之前。你先用TLA+写下“我认为这个系统会如何运行”的精确模型。如果这个模型在检证中都走不通，那就意味着你的纸面设计已经错了。这时候回去改代码是无意义的，因为代码只是忠实地执行了一份错误的蓝图。

节目中，Gergely替很多务实的工程师问出了那个关键问题：“这对初创公司、移动应用开发者有意义吗？对Web开发者有意义吗？”Hillel的回答没有任何兜售技术的狂热。他并不主张每个团队都上TLA+。他清晰地划定了一条边界：如果你面对的是并发、分布式、或者数据一致性要求极高的场景，你才会强烈地感受到它的必要。一个CRUD应用的后端、一个展示类的前端页面，你确实不需要去建模它的状态机。

这种诚实的边界感，反而让TLA+的价值显得更加锐利。它不是一颗包治百病的药丸，而是一把只用来切断最难缠的锁链的激光刀。Hillel解释，那些最复杂系统的建造者们，比如分布式数据库的作者、分布式共识协议的实现者，他们几乎无法脱离形式化方法来驾驭自己创造的东西。

AI是让形式化方法爆发，还是让它更边缘？

终于，话题进入那个AI预测的对撞地带。主流的乐观叙事是这样的：当代码由AI大量产出，人类将退回到审查者和验证者的角色。我们不再关注具体实现，但要确保机器没有产生灾难性的逻辑谬误。到那个时候，形式化证明和规约就会成为唯一可靠的守门员，需求会暴涨，工具会傻瓜化，整个领域会迎来春天。

Hillel对这个畅想的回应，冷静到几乎有些扫兴。他并不认为这一套线性推导会成立。他指出了一个被很多人忽视的根本矛盾：要让AI生成的代码去推动人类采用TLA+，逻辑上你首先需要已经有人在用。而现状是，愿意花费脑力去写出精确规约的人类工程师，本身就是极少数。如果大部分工程师在自己的日常工作中都消化不了这种思维范式，凭什么指望他们能界定、审查或信任AI产出的形式化规约？

更深一层的讽刺在于：如果AI最终确实成熟到了能替人思考所有路径交错的程度，它能做的不只是写代码，而是直接在自己的黑箱里跑完状态验证。到那个时候，你还要不要写一份外挂的TLA+规约去看懂它已经为你消化完毕的东西？于是AI可能不是让TLA+走向普及，而是直接绕过了它。Hillel的担忧就在于，这个被寄予厚望的“AI时代的形式化需求”，在最极端的情况下会直接消失，因为纠错这个动作被整合进了生成过程的内循环，再也无需人类插手。

Gergely在听完这段之后，没有试图给出一个乐观的调和。他说：“这逻辑上完全说得通，虽然这让未来走向变得更不确定了。”不确定性，恰恰正是Hillel愿意直面的事情。他不把预测当成事实，也不把流行观点当成真理。

“形式化方法就是一种写作”

如果你收听这期节目时，期待Hillel给出一个TLA+的上手指南，他会给，但给的方式极其文学化。他说：写规约，本质上是一种写作。这不是比喻，而是他反复实践后的认知。规约要给人看，也要给机器跑。而糟糕的规约，问题往往不出在逻辑上，而是出在描述上。你用了一堆自己认为理所当然的变量名、嵌套关系、状态路径，但任何另一个工程师读起来，都像在解析密文。

在他看来，好的规约和好的文章遵循同一套美学：清晰直接，不多一个字；结构明确，让读者能预测你下一步要写什么；并且，像所有好故事一样，拥有一个“让人物（状态变量）所生活的世界（不变式）稳定地持续下去”的圆满感。当Gergely追问，这种技艺是否可能被AI学会时，Hillel没有否认技术上的可能性，但点出了一个核心障碍：写清楚，需要共情——你需要知道读你规约的人会在什么地方卡住，会怎么误解。这种对误解的预判，至今依然是人类优秀作者才具备的本能。

所以整场对话落幕时，那个45行代码的画面依然印在你脑海里。它不复杂，甚至放到一个Jupyter Notebook里都显得有点寒酸。但它背后运行的，是一套将系统推向每一个可能错误边缘的逻辑。它不保证你的代码没Bug，它只是保证：如果你的设计是错的，它会让你在还没写出一行正式代码之前，就亲眼看到那个坍塌的样子。