電腦程式設計的公理基礎
像證明定理那樣，證明一個程式是對的。
要是你能「證明」一個程式沒有 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.