规格说明的回归
一段被放弃的理想
软件工程史上有一条被放弃的道路：形式化规格说明。
上世纪七十年代到九十年代，一批杰出的计算机科学家——Dijkstra、Hoare、Lamport——试图从根本上解决软件正确性问题。他们的方案是：先用数学语言精确描述程序应该做什么（规格说明），再证明实现满足这个规格（形式化验证）。Z 语言、VDM、B 方法、TLA+——这些形式化方法在学术界产生了深远影响，但在工业界几乎从未被广泛采用。
失败的原因是不划算。将意图翻译为形式化规格说明的成本太高，让规格说明跟实现保持同步，成本更高。对于大多数软件项目而言，写规格说明的时间足够把代码写两遍。于是行业选择了一条更务实的路：直接写实现，用测试来近似验证正确性，用代码审查来近似保证质量。
形式化方法退守到了航空航天、核电控制、芯片验证等失败成本极高的领域。在日常软件开发中，"规格说明"这个概念退化为产品需求文档和 API 文档——非形式化的、与实现脱节的、往往过时的自然语言描述。
这段历史的教训是：当翻译成本高于直接实现成本时，规格说明不经济。这个经济账即将被 LLM 改写。
翻译成本的急剧降低
LLM 的核心能力之一是将一种表示形式翻译为另一种表示形式。当这种翻译能力足够强时，"规格说明到实现"的翻译成本从人月降到秒。
原来导致形式化方法失败的那个原因，正在消失。规格说明之所以在工业界不经济，是因为它需要人来执行翻译。人写规格说明，人读规格说明，人将规格说明翻译为实现代码。每一步都昂贵且易错。如果机器能近乎即时地完成翻译，那么开发者唯一需要做的事情就是写出足够精确的规格说明。
今天的 LLM 辅助编程工具已经在做这件事的原始版本：开发者描述意图，模型生成实现。区别在于当前的"描述意图"大多是非形式化的自然语言，而生成的实现需要大量的人工校验和修正。但方向已经看得清——随着模型能力的提升和规格说明工具的成熟，从精确规格到可靠实现的路径将越来越短。
原始的规格语言
这个趋势的早期形态已经出现在一个意想不到的地方：CLAUDE.md 和类似的项目级指引文件。
本项目的 CLAUDE.md 本身就是一个例子。它描述了项目的定位、写作原则、技术偏好、文件命名约定、质量标准——这些都是规格说明。它告诉执行者（无论是人还是模型）"做什么"和"做成什么样"。
这类文件是原始的、非形式化的规格语言。它的局限性很明显：自然语言的模糊性导致解释空间过大，缺乏机器可验证的精确性，无法自动检查实现是否满足规格。但它的方向是对的——开发者的关注点从"怎么实现"移到了"怎么描述意图"。
第四章论证的"Code as Prompt"原则，本质上是沿同一个方向又走了一步。当 Pydantic 模型被用作 prompt 的载体时，类型注解是结构规格，Field description 是语义规格，validator 是不变量规格。这实质上是"用代码的形式化能力写规格说明"。第四章将这个思路系统化，论证了类型系统作为规格语言的完整框架。
从 CLAUDE.md 到 Pydantic 模型到 JSON Schema，形式化的程度一步步提高。一端是完全非形式化的自然语言描述，另一端是完全形式化的类型定义。当前的实践大多处于中间地带——半形式化的、混合自然语言和结构化约束的规格说明。这个中间地带不是终态，但能看出演化的方向。
声明式的尽头
照这个方向推下去，规格说明的回归将导向声明式编程的极致：开发者只描述"要什么"，实现完全由机器生成。
这个方向有先例。SQL 就是一种领域内的规格说明语言——你描述想要的数据集合的性质，查询优化器负责决定怎么获取。React 的声明式 UI 也遵循同样的模式——你描述界面在给定状态下应该是什么样子，框架负责决定怎么更新 DOM。每一次"描述意图，自动实现"的成功实践，都是规格说明思想在特定领域的验证。
LLM 提供的可能性是将这种模式从特定领域推广到通用编程。不是每个领域都需要专门设计一种声明式语言——一个足够强的翻译器可以直接将规格说明转化为任意领域的实现。
但这里有一个关键的认识论问题：规格说明的精确性要求反而提高了。
当人类程序员写实现代码时，代码本身就是最精确的规格说明——它精确到了每一个执行步骤。当开发者转向写规格说明而非实现时，规格说明中的任何模糊性都可能被 LLM 以不可预测的方式填充。第一章讨论的自然语言接口的模糊性问题，在这里就更突出了。
这意味着"写规格说明"不是一件比"写代码"更容易的事情。恰恰相反，它要求一种不同的、可能更稀缺的能力：在不触及实现细节的前提下，精确地描述意图、约束和质量标准。
从写代码到写规格
这种转变对软件工程师的能力结构有深远的影响。
传统的编程能力本质上是翻译能力：将人类意图翻译为机器指令。算法知识、语言特性掌握、API 熟悉程度——这些都是翻译效率的决定因素。当翻译可以由 LLM 完成时，这些能力的稀缺性下降。
更重要的是规格说明能力：精确定义问题空间的边界，识别和表达约束条件，在多个可行方案之间做出有依据的选择，判断实现是否满足规格。这些能力和第二章讨论的决策框架高度一致——因为规格说明本质上是一系列决策的形式化表达。
形式化方法的创始人们在四十年前就看到了这个方向。他们的错误在于低估了翻译成本这个约束条件的刚性。现在，LLM 正在削弱这个约束。那条被放弃的路又通了——这次更务实：足够精确的规格说明，加上足够强的概率性翻译器，加上足够可靠的验证机制。
形式化思想在新条件下重新具备了实用价值。精确描述意图的能力，在 LLM 时代正在从学术训练变为工程基本功。