编程语言与软件工程2018gwern.net编辑精选
软件在没有证明的情况下如何变得如此可靠？(1996)
How Did Software Get So Reliable Without Proof? (1996)
入门 · 约 45 分钟读完前置知识：软件工程基础、形式化方法概念
导读
这是 Tony Hoare 1996 年的经典演讲，探讨为什么软件在没有依赖形式化证明的情况下变得如此可靠。Hoare 认为可靠性主要来自工程实践（测试、代码审查、类型检查等）的积累，并建议形式化方法应聚焦于并发协议、资源分配等最容易出现隐蔽错误的关键领域。
HN 关注点：HN 读者长期关注形式化验证与工程实践的张力，TLA+、Rust 等话题让这篇 1996 年的旧文在今天仍有现实意义。
后来怎么样
Hoare 关于形式化方法应聚焦并发协议与资源分配等关键领域的建议，成为形式化方法在工业界应用的主导思路，影响了 TLA+ 等工具在分布式系统验证中的采用。
HN 评论精选
这几条评论里：支持 1 质疑 1 补充 2
质疑软件并非真的可靠，只是错误被规模经济和容错所掩盖
其实并没有变可靠——只是大多数错误被容忍了。不完美的自动化仍有惊人的规模经济效应，很少有应用处于受监管领域或有明确的质量标准，而且不可靠的软件至少会一致地失败，相比人类犯的创造性错误，诊断和修复流程仍然是划算的。
hcarvalhoalves查看英文原文
It didn't - but most errors are simply tolerated because imperfect automation still has absurd economy of scale, very few applications are on a regulated field or have a well-defined quality standard to meet, and unreliable software tends to at least fail consistently, so it's still a win to diagnose and fix processes compared to humans making creative mistakes.
补充Hoare 对关键领域应用形式化方法的建议预示了 TLA+ 的流行
引用论文结论：形式化方法研究者应集中精力验证大型系统中最关键的部分，例如同步与互斥协议、动态资源分配和故障恢复的重组策略。这些领域潜藏着难以测试的时序错误、死锁和活锁，可能潜伏多年后触发造成数百万损失的故障。我觉得这预示了 TLA+ 近年在从业者中的相对兴起。
Jtsummers查看英文原文
From the conclusion: > Formal methods researchers who are really keen on rigorous checking and proof should identify and concentrate on the most critical areas of a large software system, for example, synchronisation and mutual exclusion protocols, dynamic resource allocation, and reconfiguration strategies for recovery from partial system failure. It is known that these are areas where obscure time-dependent errors, deadlocks and livelocks (thrashing) can lurk untestable for many years, and then trigger a failure costing many millions. It is possible that proof methods and model checking are now sufficiently advanced that a good formal methodologist could occasionally detect such obscure latent errors before they occur in practice. Publication of such an achievement would be a major milestone in the acceptance of formal methods in solving the most critical problems of software reliability. I feel like this presages the way TLA+ (in particular) has had a relative surge among practitioners.
支持可靠性与形式化证明是两回事，工程实践才是可靠性的来源
因为可靠和证明不是同一概念，二者互不需要。证明是永恒的逻辑确定性，可靠性不是。可靠性不需要数学证明——从飞机到厨房水龙头到软件都是如此。软件通过测试、报错、修复补丁等变得越来越可靠，而且很多时候足够好就够了。
disown查看英文原文
Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good enough. We don't need the perfect for most situations. Also, it's a subjective call too. For some software is an unreliable mess and we need to throw everything out and rebuild it from scratch. Search for haskell, rust, etc threads. The neverending arguments against side-effects, mutation, pointers, etc. For most, they are good enough and get the job done.
补充形式化证明确实找到了 OpenJDK 标准库排序的真实 bug
证明正是这篇论文的作者们发现 OpenJDK 的 java.utils.Collection.sort() 有 bug 的方法（附排序正确性验证论文链接）。
thefifthsetpin查看英文原文
Proof is how the authors of this paper discovered that OpenJDK's java.utils.Collection.sort() was broken http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2018Hacker News 讨论帖83 分 · 33 评
- 2020Hacker News 讨论帖13 分 · 2 评
- 2020Hacker News 讨论帖111 分 · 123 评
同领域还值得读
Google 的软件工程（2017）
Software Engineering at Google (2017)
介绍了 Google 的软件工程实践，包括其单一代码库（monorepo）、几乎全部开发在主干进行而非分支、代码审查、构建系统 Blaze、协议缓冲区等工具与流程，并讨论了频繁重…
编程语言与软件工程2017 · 1,127 分 · 465 评 · 引用 15入门 · 约 45 分钟编辑精选Peter Naur：编程作为理论构建 (1985)
Peter Naur – Programming as Theory Building (1985)
Peter Naur 1985 年的经典论文《Programming as Theory Building》提出：编程的本质不是写代码或文档，而是在程序员头脑中构建对程序及其运行…
编程语言与软件工程2016 · 629 分 · 74 评入门 · 约 45 分钟编辑精选SciPy 1.0：Python 科学计算的基础算法
SciPy 1.0: fundamental algorithms for scientific computing in Python
这篇发表于 Nature Methods 的论文介绍了 SciPy 1.0——Python 科学计算生态的基石库，涵盖其核心算法模块（优化、积分、插值、线性代数等）、软件架构与社…
编程语言与软件工程2020 · 387 分 · 98 评入门 · 约 45 分钟编辑精选Lisp 的历史（1979）
History of Lisp (1979)
这是 Lisp 发明者 John McCarthy 于 1979 年为 HOPL（编程语言史）会议撰写的回顾文章，讲述 Lisp 的起源、设计动机与早期演进，文中也涉及 if 表…
编程语言与软件工程2018 · 352 分 · 44 评入门 · 约 45 分钟编辑精选使用 NumPy 进行数组编程
Array Programming with NumPy
这篇 Nature 文章介绍 NumPy 的数组编程模型及其在科学计算中的核心作用：以 ndarray 为中心，通过向量化操作让 Python 高效处理多维数组。
编程语言与软件工程2020 · 318 分 · 134 评入门 · 约 40 分钟编辑精选