从计算到证明：AI时代的软件工程

一、码农时代的终结

过去二十年，软件行业的主流形态是计算密集型的。业务逻辑堆砌、CRUD、框架拼接，核心能力是把需求翻译成能跑的代码，速度、产量、交付节奏是核心 KPI。类型系统、形式化方法被视为过度工程。

这很像数学史上的计算数学阶段。人们沉迷于发展更快的算法、更精巧的数值技巧，但对"为什么正确"关心不足。数学家欧拉的时代，计算能力是稀缺资源，会算就是一种权力。AI 的介入把这个计算层直接架空了。当 AI 能比你更快地写出 CRUD、更快地拼接框架、更快地生成胶水代码时，"会写代码"这个技能本身贬值了。一个残酷的事实是：AI 写代码的速度已经超过了人类阅读代码的速度，这意味着"手写"这个动作已经失去了效率意义。但这里有一个关键的反直觉后果。AI 虽然能生成代码，却不能保证代码的正确性。它的生成是基于概率的近似，而非基于逻辑的必然。于是，人类的价值被迫上移——从写代码转向验证代码。

二、从计算到证明

这正是软件行业正在经历的深层范式转移：从计算时代进入证明时代。数学史上，19世纪以前数学的核心是计算。数学家们关心的是怎么算得更快、更准。直到希尔伯特、罗素、哥德尔这一代，数学的核心问题变成了"什么可以被证明"——数学的对象从数字和公式转向了命题和证明本身。20世纪后半叶，计算机科学的诞生某种程度上是计算传统的回潮——图灵机本质上是一台计算机器。但 AI Coding 可能正在推动一场反向运动。当计算被外包给 AI，人类被迫重新面对那个更古老的问题：这东西对吗？在证明范式下，人类的核心工作不再是写实现，而是定义规约、建立不变量、论证正确性。AI 负责计算——生成代码的具体形态，人类负责证明——验证这段代码满足预设的规约。这不是分工，而是分层：计算在下，证明在上。

三、类型系统：业务无关的形式化约束

动态语言的优势在于快速生成代码，当AI将代码生产成本降低到接近于0的时候，这个优势荡然无存。于此同时，动态语言的缺点却被无限放大。动态语言的特点是弱类型和运行期检查。如果用AI大量生成这样代码，幻觉的积累往往导致错误暴露的推迟和故障半径爆炸。此时，编译型语言的静态检查特性恰好可以缓解这些问题。

类型签名是轻量级的形式化规约。当一个函数声明返回某种结果类型时，它实际上是在陈述一个命题：这个计算可能成功也可能失败，调用者必须处理两种情形。类型检查器是自动化的证明助手，它在编译期遍历代码，验证这个命题是否被遵守。编译错误是证明失败的即时反馈——不是"你写错了语法"，而是"你的论证有漏洞"。现代类型系统、所有权模型、甚至渐进类型，它们都在做同一件事：把一部分正确性从运行时转移到编译期，从测试转移到证明。测试是经验的、抽样的——我跑了一百个用例都没出问题，所以大概率没问题。证明是逻辑的、完备的——类型系统保证了这个性质在所有输入下都成立。这很像数学中从构造性证明到存在性证明的演进。我们不再关心"怎么算出来"，而是关心"是否存在、是否满足条件"。AI 负责构造——生成具体的算法和代码，人类负责存在性——论证这段代码满足规约。

四、软件和代数：形式化方法的边界

软件不是代数，两者面临的约束存在本质差异。数学是形式化的，关于强约束的。一个群论定理一旦证明，就在所有满足群公理的结构上成立，不因时代变迁而失效。数学的模型是纯粹的、自洽的、封闭的。数学家定义公理，推导定理，整个系统在一个形式化框架内运转，不需要和外部世界协商。软件及其所代表的利益却是软的、社会性的约束。软件系统嵌入在复杂的社会技术网络中，涉及多方利益相关者——用户、客户、监管者、运维团队、商业部门——每一方对"正确"的定义都不同。一个系统在技术层面无懈可击，却可能因为不符合合规要求、用户体验差、或者商业模式不匹配而被废弃。数学不关心这些，软件必须关心。

从模型建立的角度看，数学模型是对现实的抽象和简化，追求的是本质结构的揭示。软件模型却是对利益相关者需求的编码，追求的是多方约束的平衡。数学模型越抽象越好，软件模型却需要在抽象和具体之间反复折中——太抽象则无法落地，太具体则无法维护。从模型维护的角度看，数学定理一旦证明就永恒成立。软件系统却在持续演化，需求在变、环境在变、假设在变。昨天的正确性论证可能因业务规则调整而失效。软件的正确性不是一次性的证明，而是持续性的维护。形式化方法可以验证某个版本的代码满足某个规约，却无法自动处理规约本身的演化。从模型到代码的映射看，数学证明和形式化对象之间存在直接的对应关系。软件的规约和实现之间却隔着巨大的语义鸿沟。需求文档用自然语言书写，充满歧义和隐含假设；形式化规约试图消除歧义，却可能遗漏关键的社会性约束；代码实现又引入了平台特性、性能权衡、工程折中。这三层之间的映射从来不是一一对应的，形式化方法只能覆盖其中一部分。

因此，不能用代数的方法做软件。形式化验证是有力的工具，但不是万能的银弹。软件工程师需要数学的严谨精神，更需要工程的社会智慧——理解约束的来源、权衡多方利益、在不完备信息下做决策。类型系统和静态校验是这种精神的体现，但它们服务于工程目标，而非数学理想。

五、从码农回归工程师

码农的核心能力是语法熟练、框架掌握、编码速度。工作模式是接到需求、写代码、测试、交付。与 AI 的关系是被替代——AI 写得更快、更不知疲倦、不会因为加班而写出烂代码。软件工程师的核心能力是系统设计、规约定义、正确性论证、风险权衡。工作模式是理解问题、定义规约、选择验证策略、审阅 AI 生成、论证正确性。与 AI 的关系是 AI 作为执行层，人类作为决策层。工程师不排斥 AI 写代码，但工程师必须知道这段代码为什么是对的——或者至少在什么条件下是对的。同时，工程师还必须知道，这个"对"是在哪个层面的对——是类型安全层面的对，还是业务逻辑层面的对，还是社会约束层面的对。这不是说写代码消失了，而是说写代码从核心技能变成了基础技能。就像数学家不需要炫耀自己会算积分，工程师不需要炫耀自己会调 API。基础技能是门槛，不是护城河。

六、LLM 幻觉和证明必要性

要理解这个范式转移的必然性，需要回到 LLM 的本质。传统专家系统的核心特征是确定性规则。IF-THEN 链、知识图谱、符号推理。它们不会幻觉，因为它们不会生成知识库中不存在的东西。但代价是泛化能力极差——遇到规则未覆盖的情况，系统直接失效。LLM 的核心特征是伴随不确定性的泛化。基于概率分布生成文本，能够处理训练语料中从未精确出现过的模式。这种泛化能力是其智能的来源——它能类比、能迁移、能创造性地组合概念。但不确定的泛化天然携带副作用：幻觉。

幻觉与智能是一体两面。当 LLM 将一个编程概念优雅地迁移到另一个领域时，这是创造性的智能。当它自信地生成一个不存在的 API 调用时，这是破坏性的幻觉。两者的机制完全相同，都是概率模型在分布外区域的推断，区别只在于结果是否恰好符合现实。我们无法剥离幻觉而保留智能，正如我们无法只取火的热量而拒绝它的灼伤。

既然幻觉是 LLM 能力的内禀属性而非可修复的缺陷，工程策略就不应该是消除幻觉，而应该是构建系统使得幻觉的代价可控、范围有限、可被快速检测。这正是静态类型系统的价值所在——类型签名将 AI 的生成空间限制在形式化合法的范围内，编译期错误让幻觉在投入运行前暴露，类型隔离确保一个模块的幻觉不会无声地污染整个系统。

但类型系统只能约束形式层面的幻觉，无法约束语义层面的幻觉。AI 可能生成类型正确但业务逻辑荒谬的代码，可能生成满足接口契约但违背用户期望的系统。这正是软件与代数的分野所在——形式正确只是必要不充分条件，社会正确才是最终判据。类型系统是防火墙，不是终点站。

七、软件工程教育的未来图景

也许未来的软件工程教育会像数学教育一样分层，但必须保留软件的社会维度。基础层是形式逻辑、类型理论、离散数学——证明的基本功。不是作为"计算机科学的基础"来学，而是作为"工程师的核心能力"来学。但同时，必须并行学习需求工程、利益相关者分析、系统设计伦理——理解软件不是活在真空中的形式系统。工程层是系统设计、分布式一致性、安全模型——如何规约复杂系统。不是学"怎么搭微服务"，而是学"怎么论证这个微服务架构在分区容错下保持一致性"，以及"这个一致性模型对业务场景是否过度或不足"。工具层是 AI 协作、形式化验证工具、静态分析——如何高效地证明。但工具的使用必须嵌入在工程判断中：什么时候值得形式化验证，什么时候测试就够了，什么时候甚至应该接受未验证的风险。而语法细节、框架用法、调试技巧——这些曾经占据面试核心的问题，可能会像手算开方一样，成为历史注脚。不是因为它们不重要，而是因为它们已经被工具化、被自动化、被外包了。

八、结语

AI 不是在消灭软件工程，而是在把它从手艺活还原为工程学科。而工程学科的本质，从来都不是做出来，而是证明它是对的——在特定的约束下、对特定的利益相关者、在可接受的风险范围内。

从码农回归工程师，从计算到证明，从运行时调试到编译期验证——这个回归不是倒退，而是螺旋上升。软件行业花了二十年学习如何快速建造，现在它需要重新学习如何保证正确。类型系统是这个回归的技术表征，静态校验是这个回归的工程实践，而对正确性的敬畏是这个回归的精神内核。

但软件工程师必须比数学家多走一步。数学家证明了对就是对了，软件工程师证明了对之后，还要问：对谁对？在什么条件下对？当条件变化时还能维持吗？这些问题的答案不在类型系统里，而在工程师对复杂社会技术系统的理解中。

也许有一天，我们会像数学家谈论证明一样谈论软件——不是"这段代码能跑吗"，而是"这个系统满足规约吗"。AI 负责构造答案，人类负责验证答案，同时负责定义问题本身。这曾经是数学的分工，现在正成为软件工程的分工。但软件工程永远会比数学多一层：证明之后，还要交付。