01 · 计算人生
成果背后的人
罗伯特·弗洛伊德推动以严格的数学推理研究程序正确性。他发展了在程序步骤上附加逻辑断言、证明计算符合规格的方法。他还研究算法、语法分析和程序综合。在斯坦福，他推动一种把高效计算过程与关于其行为的严谨论证共同发展的计算机科学研究方式。
理解这项贡献
罗伯特·弗洛伊德帮助建立了软件构造的数学语言。断言描述计算中某个位置应当成立的条件。将这些条件与程序操作联系起来，就能推理正确性，而不只是观察若干次运行。他的贡献还涉及语法分析、语义和算法分析。
为什么重要
程序验证和精确的语言工具，让可靠软件成为能够系统研究的对象。