计算机程序设计的公理基础
像证明定理那样，证明一个程序是对的。
要是你能「证明」一个程序没有 bug 呢——不是测它一千遍然后祈祷，而是像证明一条数学定理那样，把它证出来？
把这个想法拆开看
大多数软件靠测试来检查：拿一些输入跑一跑，看看答案对不对。可测试至多只能说明：你试过的那些情形是对的——它永远说不清你没试到的那一种会不会崩。霍尔提出了更强的东西：用朴素的逻辑写下——一段代码运行「之前」必须为真的是什么、运行「之后」会为真的是什么——再用滴水不漏、一次覆盖所有可能输入的推理，把这两头连起来。
他把它写成一个小小的「三明治」：前置条件、程序、后置条件。任何程序里最难缠的部分都是循环，因为它可以跑任意多次。霍尔对付循环的关键工具，是「不变式」——一条无论循环转多少圈、每一遍都保持为真的陈述。把对的不变式钉死，循环的正确性也就随之落地。
它从哪里来
1969 年，托尼·霍尔——已因发明 Quicksort 快速排序算法而成名——是贝尔法斯特女王大学一位年轻的教授。在弗洛伊德 1967 年「把逻辑断言挂到流程图上」的想法之上，霍尔以欧几里得几何的风范，把整件事重铸了一遍：用寥寥几条公理与规则，便能推导出一个程序的正确性。
他对署名归功很谨慎，特意指出：断言这个想法，经由弗洛伊德，可一路上溯到 1940 年代的图灵与冯·诺伊曼。而他自己的天赋之笔，是那组优雅的规则——一条管赋值，一条管步骤的串接，一条管循环——它们让这套方法干净到可以拿来教学，又通用到足以传世。
它为何重要
正是在这一刻，编程开始从一门手艺，变成一门科学。霍尔的开篇之句——一个程序的行为，原则上可以单凭推理、从它的文本里推算出来——立下了一个此后这一领域始终追逐的理想。对于那些绝不容许失败的软件（飞机、医疗器械、你车里的芯片、操作系统的内核），「我们测了很多」远远不够；「我们证明了」才是黄金标准——而霍尔，给了我们做这件事的语言。
一个打比方
想象一架天平，你得在挪动砝码的同时始终让它保持水平。循环不变式，就是一个承诺：每挪动一次之后，天平依然平衡，哪怕砝码一直在变。在霍尔自己的例子里——用反复相减来做除法——这个承诺是：「我拿走的那部分，加上还剩下的那部分，永远等于我一开始的那个数。」它在起点成立，在每一次相减之后也成立，而当你再也减不动时，它就把答案告诉了你。
它处在何处
霍尔的逻辑，是关于「计算机与逻辑能做什么」这一宏大三重奏中的一条腿。图灵（1936）证明了：有些问题，任何程序都永远答不出来；哥德尔（1931）证明了：有些真理，任何形式系统都永远证不出来。在这样的底色之上，霍尔圈出了光明的一面：对于我们实际写下的那些程序，正确性是可以被证明的。与他几乎同代的艾兹格·迪杰斯特拉（他 1959 年的最短路径工作也在本馆中）高举着同一面旗——「结构化编程」，以及边写边对程序作推理、而非写完之后再说。
In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics.
Computer programming is an exact science in that all the properties of a program and all the consequences of executing it in any given environment can, in principle, be found out from the text of the program itself by means of purely deductive reasoning.
If the assertion P is true before initiation of a program Q, then the assertion R will be true on its completion.