今天，我们已经习惯让程序处理银行交易、控制汽车、分配云端资源，甚至生成新的程序。但如果把时间拨回计算机尚未诞生的年代，一个更根本的问题仍悬而未决：所谓“按照步骤完成计算”，究竟是什么意思？哪些问题可以交给机器，哪些问题无论给它多少时间也无法解决？
这个好奇心后来引出了一条意想不到的历史线索。数学家先用纸笔想象机器，程序员随后发明语言命令真实的机器；当程序越来越长，人们又不得不追问一句代码“意味着什么”，以及一段程序为什么值得信任。程序语言形式化（formalization of programming languages）正是在这些追问中逐渐成形的。
这段历史并不是几位学者依次提出几个术语的年表。每一种新方法，几乎都来自旧方法遇到的麻烦：自然语言无法精确规定语言行为，于是出现程序语义；测试无法覆盖所有路径，于是出现程序证明；完整证明难以推广到海量代码，于是出现自动分析。沿着这些麻烦回看，今天论文里的操作语义（operational semantics）、霍尔逻辑（Hoare logic）、不动点（fixed point）与抽象解释（abstract interpretation），也就不再是突然落在页面上的符号，而是一次次工程困境留下的答案。
一、计算机出现以前：什么才算“可以计算”？
20 世纪初，数学家希望把数学推理建立在严格的形式系统之上。一个很自然的愿望是：能否设计一套机械步骤，只要输入一个数学命题，就能判断它是否成立？这里的“机械”并不是比喻，而是要求每一步都足够明确，不依赖灵感，也不允许执行者临时猜测。
问题很快卡在一个看似普通的词上：什么叫“机械步骤”？如果不先定义计算，便无法证明某个问题可计算，更无法证明它不可计算。
1930 年代，阿隆佐·丘奇（Alonzo Church）用 λ 演算（lambda calculus）研究可计算函数；艾伦·图灵（Alan Turing）则设想了一位严格照表工作的计算者：他读取纸带上的符号，根据当前状态写入符号、左右移动，再进入下一个状态。这个模型后来被称为图灵机（Turing machine）。两条思路表面上差异很大，却刻画出同一类可计算函数，由此形成了丘奇—图灵论题（Church–Turing thesis）的基础。
艾伦·图灵，摄于 1951 年。
图灵的模型最有力量的地方，不是它像今天的电脑，而是它把“执行一个算法”拆成了有限、局部且无歧义的动作。机器在某一步的全部情况，可以写成一个配置：
\[C=\langle q,\;t,\;i\rangle,\]其中 $q$ 是控制状态，$t$ 是纸带内容，$i$ 是读写头位置。转移规则再说明配置 $C$ 如何变成下一配置 $C’$：
\[C\longrightarrow C'.\]这已经很接近今天程序语义的基本形状：先定义状态，再定义一步计算，最后研究许多步计算会到达哪里。换句话说，在真实的通用计算机出现之前，描述程序执行所需的形式化骨架已经出现了。
图灵论文里的 “computer” 起初指的不是电子设备，而是执行计算工作的人。图灵把这位计算者能观察和记住的内容压缩到极少，再把动作写成规则。后来被视为机器蓝图的模型，最初其实来自对人类拿着纸笔计算的细致观察。可参阅图灵的原始论文 On Computable Numbers。
这段早期历史还留下了一个重要边界：并非所有写得出来的问题都存在通用算法。形式化从一开始就不只告诉我们“机器能做什么”，也告诉我们“不要期待机器做到什么”。后来关于程序终止性、验证自动化和分析精度的许多限制，都可以在这里找到源头。
二、程序语言诞生：语法先变得精确，意义仍留在文字里
电子计算机投入使用后，程序最初与具体机器紧密绑定。程序员直接面对指令、地址与跳转，换一台机器往往就要重写代码。20 世纪 50 至 60 年代，FORTRAN、Lisp 和 ALGOL 等高级程序语言陆续出现，程序开始脱离某一台机器，成为可以独立讨论的文本对象。
1957 年，美国国家航空咨询委员会（NACA）的工作人员操作 IBM 704。早期 FORTRAN 正是围绕 IBM 704 开发的。
这带来了一个新问题：一门语言怎样才能让不同的人、不同的编译器得到相同理解？
ALGOL 60 的报告以巴科斯—诺尔范式（Backus–Naur Form，BNF）精确描述语法。赋值、条件、循环和过程不再只靠例子解释，而是由产生式规定哪些符号组合属于合法程序。这一步极其重要，因为它把“程序长什么样”从编译器实现中抽离出来，成为公开、可检查的语言定义。
然而，语法只能判断一句话是否写得合法，不能完整说明它运行时会发生什么。例如，下面的赋值符合语法：
1
x := x + 1
但要理解它，还需回答：右侧表达式何时求值？变量对应的存储位置是什么？整数溢出怎样处理？如果表达式没有定义，程序应当停止还是产生某个值？这些问题若仍依靠自然语言说明，不同实现就可能在边界处产生不同结果。
ALGOL 60 报告对语法的描述非常精确，动态行为却仍大多用自然语言说明。这种“语法已经形式化、意义仍靠文字解释”的反差，恰好说明了下一步为什么困难：列出合法句子相对容易，解释所有合法句子的行为则需要一套更强的数学语言。
当时的研究者逐渐意识到，语言定义不能只像一本语法书，还要像一个数学模型：每个程序构造都应有明确含义，而且复杂程序的含义应当能够由其组成部分推导出来。程序语义（program semantics）由此走到舞台中央。
三、给程序寻找“意义”：两种描述程序的地图
“这段程序是什么意思？”没有唯一的回答方式。有人选择描述它怎样一步步执行，有人则关心它最终代表哪个数学对象。后来，这两种视角分别发展为操作语义和指称语义。
它们不是相互淘汰的两代技术，而像观察同一座城市的两张地图：路线图适合追踪怎样从一站走到下一站，地形图适合理解不同地点在整体空间中的关系。选择哪一种，取决于我们准备回答什么问题。
3.1 操作语义：程序怎样一步步走
操作语义（operational semantics）把程序行为写成状态之间的转移。若 $\sigma$ 表示变量到值的映射，那么赋值语句可以写成：
\[\langle x:=e,\sigma\rangle \longrightarrow \langle \texttt{skip},\sigma[x\mapsto [\![e]\!](\sigma)]\rangle.\]这条规则读作：在状态 $\sigma$ 中执行 x := e，先计算表达式 $e$，再用结果更新 $x$，语句执行完毕后变成 skip。循环、分支、函数调用也可以用类似规则逐层定义。
操作语义的优势是贴近执行。设计解释器、说明并发程序的交错、证明编译前后行为一致时，我们往往需要看见每一步发生了什么。戈登·普洛特金（Gordon Plotkin）在结构化操作语义（structural operational semantics，SOS）中进一步系统化了这种写法：复杂语句的行为由子语句的规则组合而成。今天论文中常见的推导横线与转移箭头，大多延续了这套表达习惯。
3.2 指称语义：程序最终代表什么
指称语义（denotational semantics）选择另一条路：不模拟机器动作，而把每个程序片段映射到一个数学对象。例如，一条命令可以被解释为从初始状态到最终状态的函数：
\[[\![c]\!]:\Sigma\rightarrow\Sigma.\]如果两个程序映射到相同对象，就可以在这个模型中把它们视为具有相同意义。更重要的是，复合语句的含义由局部含义组合而来：c1; c2 的意义就是两个状态变换的复合。这种组合性（compositionality）让研究者不必每次都把整个程序摊开，而能从部件推导整体。
克里斯托弗·斯特雷奇（Christopher Strachey）与达纳·斯科特（Dana Scott）在 1960 年代末至 1970 年代初推动了这条道路。递归程序带来一个棘手问题：一个函数的定义会引用自己，它的“意义”怎样避免循环定义？斯科特发展的域理论（domain theory）用偏序和不动点为递归提供了数学基础。我们今天在程序分析里遇到格、单调函数和最小不动点，并不是偶然借用的一组工具；它们曾经就是为解释递归计算而进入程序语言理论的。
斯科特与斯特雷奇在论文中坦率地记录过一个尴尬：早期语义直觉已经出现，但他们使用的某些“函数空间”未必能用普通集合论直接构造。应用反过来迫使数学基础升级。形式化的发展并非总是“理论先行”，有时是程序提出了问题，数学才不得不追上来。可参阅 Toward a Mathematical Semantics for Computer Languages。
到这里，人们已经能够讨论程序怎样运行，以及程序在数学上表示什么。但当软件从实验室里的计算工具变成需要交付和维护的系统，问题很快又向前推进了一步：知道程序“是什么意思”还不够，我们能否证明它符合要求？
四、软件突然长大：“能运行”不再等于“可信”
程序语义并非只由数学家的审美推动。1960 年代，软件系统的规模和重要性迅速上升，项目延期、成本失控、可靠性不足等问题变得无法忽视。1968 年在德国加米施举行的北约软件工程会议（NATO Software Engineering Conference），把来自多个国家的研究者和产业人士聚在一起，讨论大型软件的设计、生产、分发与维护。
那份会议报告读起来不像一份结论整齐的宣言，而更像一间争论激烈的会议室：有人担心软件已经进入社会关键系统，有人讨论为什么进度和规格总是失守，也有人争论软件是否应当与硬件分开计价。后来常用“软件危机（software crisis）”概括那个时代，但危机背后的核心变化更具体——软件不再只是少数专家可在脑中完整掌握的小程序。
测试当然重要，却只能展示已经运行过的情况。一个程序通过一万次测试，不等于第一万零一次不会触发遗漏的路径。面对分支、循环与输入组合，正确性需要一种能覆盖一类执行、而不是一次执行的论证。
4.1 公理语义：不问每一步，只问前后是否成立
罗伯特·弗洛伊德（Robert Floyd）与托尼·霍尔（Tony Hoare）的工作为这种论证提供了语言。它们并不是由某一次会议直接催生的，却与那个时代对软件可靠性的焦虑汇聚到了一起。弗洛伊德在 1967 年展示了如何在流程图的关键位置附加断言，并证明控制沿边移动时断言仍然成立；霍尔在 1969 年把这些思想组织成针对程序构造的公理与推理规则。
公理语义（axiomatic semantics）把注意力从完整执行过程转向程序性质。与其列出命令 c 的每一步，不如说明：若执行前满足前置条件 $P$，且程序能够结束，那么执行后满足后置条件 $Q$。这就是霍尔三元组（Hoare triple）：
例如：
\[\{x=0\}\ x:=x+1\ \{x=1\}.\]证明一个循环时，也不必枚举它执行零次、一次或一百万次的所有轨迹，而是寻找一个循环不变量（loop invariant）：进入循环前成立，每轮执行后仍成立，并且在退出时足以推出目标性质。有限的证明因此可以约束无限多次潜在迭代。程序由此不只是可以运行的文本，也成为可以证明的对象。
4.2 戴克斯特拉：让规范参与程序构造
艾兹赫尔·戴克斯特拉（Edsger W. Dijkstra）随后把“先写程序、再证明它”进一步推向“从目标性质推导程序”。他的最弱前置条件（weakest precondition）思想从期望的后置条件 $Q$ 反向计算：为了让命令 $c$ 执行后保证 $Q$，执行前至少要满足什么？
\[wp(c,Q)=P.\]这改变了正确性的角色。规范不再是程序完成后附加的一张检查表，而可以参与程序的构造。结构化程序设计（structured programming）之所以与形式推理关系紧密，也正因为顺序、分支和循环具有可组合的控制结构，更容易为执行进度找到清晰坐标。
戴克斯特拉1994年在苏黎世联邦理工学院讲解程序推导，左侧可以看到带守卫命令的程序及其性质。
戴克斯特拉提交给期刊的原题是 A Case against the GO TO Statement。编辑尼克劳斯·维尔特（Niklaus Wirth）把它改成了后来著名的 Go To Statement Considered Harmful，“X considered harmful”也意外成为沿用数十年的标题模板。戴克斯特拉后来笑称，许多人恐怕只读过标题，甚至还有文章叫“Dijkstra considered harmful”。这段回忆可见 EWD1308。
五、纸上的证明开始进入机器
证明程序比运行几个测试更全面，但手写证明同样会出错。证明变长以后，读者可能漏看一个前提、误用一条规则，或在数百步推导中犯下不起眼的替换错误。既然证明已经由形式规则组成，一个自然的问题便出现了：能否让计算机检查证明本身？
5.1 小内核：把信任集中到很小的地方
1972 年，罗宾·米尔纳（Robin Milner）开发了斯坦福 LCF（Logic for Computable Functions）。它后来形成一种影响深远的证明助手架构：系统可以使用复杂策略寻找证明，但只有一个很小的可信内核能够产生“定理”这一受保护对象。策略即使有缺陷，最多导致证明失败；只要绕不过内核，就不能凭空制造一个已经证明的结论。
这个设计把“相信整套庞大自动化软件”改成“相信一个尽可能小的检查器”。米尔纳团队为编写证明策略设计的元语言，后来发展成 ML 语言。于是，程序语言、类型系统和证明工具在同一个项目里发生了耐人寻味的汇合：为了更可靠地证明程序，人们又创造出新的程序语言。
早期 LCF 不只受限于计算速度，保存完整证明还会迅速耗尽内存，固定的证明命令也难以扩展。爱丁堡 LCF 的改进没有简单追求“让机器自动证明一切”，而是让人编写灵活的策略、让小内核负责最后核验。这种“强大的搜索，克制的信任”至今仍是许多证明助手的设计哲学。可参阅剑桥大学的 LCF 与 HOL 简史。
5.2 证明与程序原来可以使用同一种语言
另一条线索来自柯里—霍华德对应（Curry–Howard correspondence）：命题可以看作类型，证明可以看作拥有该类型的程序。证明命题的过程，于是对应于构造一个满足相应类型的项；检查证明，则可以转化为类型检查。
这条联系影响了 Coq、Agda、Lean 等证明助手，也让类型系统的角色发生扩展。类型不再只是区分整数和字符串，还可以表达列表长度、资源状态、协议阶段乃至函数输入输出之间的关系。形式化规范、程序实现与正确性证明开始能够出现在同一个框架中。
当然，机器检查不等于机器包办。人仍需选择恰当的定义、引理和抽象，自动化工具则承担机械推导与一致性检查。分工发生了变化：创造性的部分仍由人引导，容易出错的细节交给机器守门。
六、证明太贵以后：怎样自动分析更多程序？
到这里，形式化似乎已经给出了理想答案：为程序写规范，再由证明助手核验。但大型软件包含数百万行代码、第三方库和持续变化的需求，逐行构造完整证明通常成本很高。工程实践需要另一种能力：即使得不到程序的全部真相，也要自动、可靠地回答某一类关键问题。
6.1 抽象解释：用可计算的近似换取规模
1977 年，帕特里克·库索（Patrick Cousot）与拉迪娅·库索（Radhia Cousot）提出抽象解释的统一框架。它的核心并不是“随便忽略一些细节”，而是把具体执行映射到一个更小的抽象世界，并保证抽象结论能够安全覆盖具体行为。
帕特里克·库索，摄于 2007 年。
假设程序变量可能取任意整数，具体状态近乎无穷。若分析目标只关心正负，就可以把所有整数压缩成少量抽象值：
\[\mathbb{Z}\quad\Rightarrow\quad \{\textsf{Neg},\textsf{Zero},\textsf{Pos},\top,\bot\}.\]分析器不再追踪 x = 173，而是记录 x 为正。它失去具体数值，却保留回答符号问题所需的信息。不同路径在控制流汇合处用合并操作（join）汇总，循环则通过不动点计算得到稳定结果；若抽象域存在无限上升链，还可用加宽（widening）帮助迭代停止。
这套框架把语义与算法连在了一起：程序语义说明具体执行是什么，抽象关系说明哪些细节可以忘记，格结构和不动点则说明近似结果怎样计算。空指针分析、区间分析、污点分析与许多编译器数据流分析虽然目标各异，却可以在同一幅理论地图上理解。库索夫妇的原始论文还特意用“符号规则”解释抽象执行，今天读来仍很直观，可参阅 1977 年的论文与摘要。
如果想回到技术细节，可以接着阅读本系列的 不用记住每个值——从具体状态走向抽象解释 和 分析器为什么会停下来？从 Transfer Function 到不动点。
6.2 模型检测：让机器系统地搜索状态空间
几乎在同一时期，模型检测（model checking）走出另一条自动化道路。研究者把系统表示成有限状态模型，把“永远不会进入错误状态”“请求最终会得到响应”等性质写成时序逻辑（temporal logic），再由算法系统搜索状态空间，判断模型是否满足性质；若不满足，工具通常还能给出一条反例路径。
模型检测的吸引力在于反馈具体：工程师不只得到“证明失败”，还可能看到系统如何一步步走进错误。但它也受到状态爆炸（state explosion）的困扰——几个组件组合后，整体状态数会急剧增长。此后的符号表示、偏序约简和有界模型检测等技术，都在与这个规模问题周旋。
2007 年，埃德蒙·克拉克（Edmund Clarke）、艾伦·爱默生（E. Allen Emerson）与约瑟夫·斯发基斯（Joseph Sifakis）因推动模型检测成为广泛使用的验证技术获得图灵奖。这也标志着形式化方法不再只是纸面理论，而已经能够进入硬件与软件工程流程。
七、形式语义走进现实系统
进入 21 世纪后，程序语言形式化并没有被更强的测试或更快的硬件取代，反而以更不显眼的方式进入工程基础设施。现代编译器优化需要证明变换不会改变程序可观察行为；并发系统需要定义消息、锁与内存访问的交互；安全协议需要说明攻击者能知道什么；类型检查器与静态分析器则每天在编辑器和持续集成中运行。
CompCert 是一个具有代表性的例子。它为接近完整 C 语言的源程序和多种目标汇编定义形式语义，并在 Coq 中证明编译过程保持程序行为。这里被验证的不是某一个应用，而是承载大量应用的编译器：一旦编译器错误地改变代码，仅证明源程序正确还不够。CompCert 的目标正是缩小这段信任缺口。
这段历史也改变了我们理解“形式化成功”的方式。成功不一定意味着把整个世界塞进一个巨大证明；它也可能是找到合适的可信边界：为语言标准澄清一种模糊行为，为协议的核心状态机建立模型，为分析器证明无漏报性质，或让一个小内核检查外部工具产生的证明证书。
形式化语义有时会暴露实现者早已习惯、标准却没有说清的角落。不同编译器对同一段边界代码给出不同结果时，问题未必是谁“写错了”，也可能是大家一直依赖的文字规范留下了歧义。此时，写下一条明确的语义规则，本身就是一种工程修复。
从这个角度看，操作语义、指称语义和公理语义也不必争夺唯一正确的位置。一个经过验证的编译器可能用操作语义定义源语言和目标语言，用逻辑关系或模拟关系连接两边，再借助证明助手检查推导。静态分析器则可能从收集语义出发，经由抽象解释得到可执行算法。成熟工具往往不是站在某一个学派内部，而是按任务组合这些思想。
八、回看这段历史：改变的不是符号，而是提问方式
从 1930 年代到今天，程序语言形式化反复面对同一个矛盾：真实程序太复杂，直觉无法完整掌握；但如果模型保留所有细节，又会和真实程序一样难以处理。每一次重要进展，都在重新选择“保留什么、忽略什么、由谁检查”。
图灵机忽略物理机器的材料，只保留计算步骤；指称语义忽略具体执行轨迹，把程序映射到数学对象；霍尔逻辑忽略许多运行细节，只追踪与规范有关的前后条件；抽象解释进一步有目的地压缩状态，用精度换取自动化和规模；证明助手则不替人决定什么值得证明，而是把最终推导交给小内核核验。
因此，形式化方法的历史并不是数学不断取代编程的历史，而是人类逐渐学会怎样与复杂性谈判。我们无法把所有细节同时握在手中，于是发明语义来固定含义，发明逻辑来组织论证，发明抽象来控制规模，再发明机器检查来约束自己的错误。
今天再读一条形式化规则，可以多问几个历史留下的问题：作者选择了什么作为状态？规则描述的是执行过程、数学意义，还是前后性质？哪些细节被抽象掉了？结论依赖人工论证、自动搜索，还是一个可检查的证明？这些问题比记住某位学者在哪一年提出哪个术语更重要，因为它们仍在塑造新的语言、分析器和验证系统。
也许未来的程序主要由自然语言描述，由大模型生成，再交给验证器检查；也许语言本身会携带更丰富的规范与证明。但无论界面怎样变化，只要我们仍需要回答“它会做什么”与“为什么可以相信它”，这段从纸带、断言到抽象状态的历史就还没有结束。
历史留下的核心直觉
形式化不是把程序写得更像数学，而是为“程序意味着什么、可能怎样运行、为何满足要求”建立一种可以反复检查的共同语言。
九、进一步阅读
如果想沿着历史线索继续追溯，下面这些原始材料比二手年表更能呈现当时的问题意识。无需一次读完，可以按感兴趣的节点选择：
- 艾伦·图灵，《论可计算数及其在判定问题上的应用》（On Computable Numbers, with an Application to the Entscheidungsproblem，1936/1937）。
- 北约科学委员会，《1968 年北约软件工程会议报告》，适合直接感受早期大型软件工程中的争论。
- 罗伯特·弗洛伊德，《为程序赋予意义》（Assigning Meanings to Programs，1967）。
- 托尼·霍尔，《计算机程序设计的公理基础》（An Axiomatic Basis for Computer Programming，1969）。
- 达纳·斯科特与克里斯托弗·斯特雷奇，《走向计算机语言的数学语义》（Toward a Mathematical Semantics for Computer Languages，1971）。
- 戈登·普洛特金，《操作语义的结构化方法》（A Structural Approach to Operational Semantics，1981）。
- 帕特里克·库索与拉迪娅·库索，《抽象解释：基于程序不动点构造或近似的统一格模型》（1977）。
- CompCert 项目，经过形式化验证的 C 编译器介绍，可以观察语义与机器证明如何进入现实编译器。
