编程语言与软件工程2020cslab.pepperdine.edu
Amazon Web Services 如何使用形式化方法（2015）
How Amazon Web Services Uses Formal Methods (2015)
进阶 · 约 40 分钟读完前置知识：分布式系统基础、并发与一致性、TLA+/模型检验概念
导读
这篇论文介绍亚马逊 AWS 如何把 TLA+ 形式化方法用于系统设计：工程师先用 TLA+ 写出设计的可穷举检验的“伪代码”模型，用模型检验器在编码前找出并发与故障场景下的设计缺陷，再据此实现真实系统。文中以 DynamoDB、S3 等十余个复杂系统为例，说明形式化方法从设计阶段就介入，并报告了它带来的收益。
HN 关注点：工业界真实落地经验：形式化方法是否拖慢开发、普通工程师能否学会，以及它对系统正确性的实际价值。
后来怎么样
这篇论文成为工业界采用形式化方法的标志性案例，推动了 TLA+ 在 AWS 之外分布式系统团队中的传播，也让“设计阶段用模型检验找并发与故障缺陷”更广泛地进入云系统工程实践。
HN 评论精选
这几条评论里：补充 3 亲历 1
亲历亲历者称 TLA+ 不仅没拖慢开发，反而加速了实现并提升了正确性信心。
我在 AWS 工作时，有个团队在新后端功能上用了 TLA+。这个功能一旦出问题对客户影响极坏，加上要在大规模下运行，复杂度更高，因此必须高度警惕。原本乐观估计要 4 个月。任务交给两位资深开发者，他们得从零学 TLA+ 和形式化方法（其中一人主要抱怨是被迫用 Eclipse）。适应花了一点时间，但很快他们就能在设计中实现并抓 bug，几周内就把所有 bug 清干净了。随后他们发现从 TLA+ 转到实际 Java 代码几乎就是“填空”：形式化模型几乎给出了最终代码所需的结构，写代码花的时间很少。不到两个月系统就以 shadow 模式在生产环境运行，不久后完全上线。TLA+ 后来又被用于平台的其他多个功能。此前开发者普遍认为学 TLA+ 做形式化验证只会拖慢进度，但我们发现恰恰相反：它实际上加快了开发，还带来更高正确性信心这一大好处。
Twirrim查看英文原文
One of the teams I worked for in AWS used TLA+ on a new back-end feature that was added. It was one that, if things went wrong, would be extremely bad for customers. The needs for operating on scale only added to the necessary complexity. Paranoia was key. They'd estimated something like an optimistic 4 months for the work. Two of the more senior developers were assigned the task, and they had to learn TLA+ and formal methods from scratch. (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then). It took a little bit for them to get up to speed, but they were soon implementing and catching bugs in the proposed designs, and they had all the bugs ironed out within a few weeks. They then found that going from TLA+ to actual Java code was almost a "fill in the blanks" exercise. The formal model provided almost the exact structure they needed for their final code. Going from model to code took them very little time at all. It was in production, running in shadow mode after not even 2 months, and was fully live not long afterwards. TLA+ got subsequently used for a number of other features added to the platform. There had been general push back among developers that learning TLA+ and doing formal verification was only going to slow them down, but we found it was quite to the opposite. TLA+ actually sped up development, with the big bonus of higher confidence of correctness.
补充补充了 AWS 自动化推理与可证明安全相关的演讲和资料链接。
自动化推理组首席科学家 Bryon Cook 概述了 AWS 目前使用的各种求解器：https://www.youtube.com/watch?v=UKqVY0SSbus 。还有杰出工程师 Eric 和首席工程师 Neha 关于分析 IAM 策略（Zelkova？）和网络可达性（Tiros？）的演讲：https://www.youtube.com/watch?v=x6wsTFnU3eY 。这个网页有更多相关博客文章链接：https://aws.amazon.com/security/provable-security/
ignoramous查看英文原文
Bryon Cook, a principal scientist at Automated Reasoning Group gives an overview of various solvers in-use today at AWS: https://www.youtube.com/watch?v=UKqVY0SSbus Here's a presentation by Eric, a distinguished engineer, and Neha, a principal engineer, on analysing IAM policies (Zelkova?) and Network reachability (Tiros?): https://www.youtube.com/watch?v=x6wsTFnU3eY This webpage has many more links to blog articles on the topic: https://aws.amazon.com/security/provable-security/
补充梳理论文要点：TLA+ 只用于设计而非实现，DynamoDB 和 S3 等系统在用，且有工程师曾自造暴力检验器。
我读论文到结尾才得到答案的几个问题：问：工程师真的用 TLA+ 实现 AWS 系统吗？答：不，TLA+ 内部被称为“可穷举测试的伪代码”，只用于设计。问：哪些 AWS 系统用了它？答：最早是 DynamoDB，然后是 S3，现在另有 8 个复杂系统用它做设计。问：亚马逊谁在用 TLA+？答：所有工程师，从入门到首席。我觉得特别有意思的是，AWS 有几位工程师实际上在写自己的模型检验器，用程序暴力尝试会导致系统失败的罕见条件组合。显然 TLA+ 做得更好更快，所以他们转向了它。
lwb查看英文原文
Questions I wondered about that weren't answered until the end of the paper: Q: Do engineers actually implement AWS systems in TLA+? A: No, TLA+ is called "exhaustively testable pseudo-code" internally, and is only used for designs. Q: Which AWS systems use it? A: The first was DynamoDB, followed by S3, and now there are 8 additional complex systems that use it for designs. Q: Who uses TLA+ at Amazon? A: All engineers, from entry level to principal. I thought it was especially interesting that several engineers at AWS were effectively writing their own model checkers by writing programs that tried to brute force rare combinations of conditions that would lead to system failure. Obviously TLA+ does this better and faster so they switched to that.
补充推荐 TLA+ 学习资源，并称其比 Isabelle、Coq 更易上手。
我业余时间开始用 TLA+。有几个不错的学习网站和书：https://learntla.com/introduction/ 、《Practical TLA+》。它比 Isabelle、Coq 等其他形式化方法工具容易上手得多。
exdsq查看英文原文
I’ve started using TLA+ in my spare time. There are several good sites and books to learn more about it: - https://learntla.com/introduction/ - Pracitcal TLA+ It’s much easier to get running with than other formal methods tools like Isabelle and Coq.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2020Hacker News 讨论帖199 分 · 28 评
同领域还值得读
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 分钟编辑精选