01 · 计算人生
成果背后的人
托尼·霍尔提出了让程序更快、也更容易推理的方法。他发明快速排序，并建立描述程序运行前后应满足条件的逻辑。他后来研究通信顺序进程，为并发系统提供理论框架。在牛津，他把语言设计、形式化规格与验证结合起来，持续推动提高软件可靠性。
理解这项贡献
托尼·霍尔发展了程序语言和程序推理中的基础思想。霍尔逻辑将一条命令与运行前、运行后应当成立的条件联系起来。他的工作还包括快速排序和通信进程模型。图灵奖表彰的是他在程序设计定义与发展上的广泛贡献。
为什么重要
明确的契约帮助人们理解部件如何组合，以及正确实现必须保持什么。