编程语言与软件工程2024lamport.azurewebsites.net
TLA+ 的未来
The Future of TLA+
进阶 · 约 45 分钟读完前置知识：TLA+ 基础、形式化方法基础、分布式系统基础
导读
这是 Leslie Lamport 关于 TLA+（一种用于描述系统行为的数学化形式规约语言）未来发展方向的论文。文中阐述了 TLA+ 的设计理念，如强调简洁性、坚持“它是数学而非编程语言”的定位，并解释了为何许多方面无需改变。
HN 关注点：形式化验证工具的演进方向，讨论焦点集中在 TLA+ 是否真的“简单”、其数学定位是否合理，以及未来是否需要语法和生态上的革新。
HN 评论精选
这几条评论里：质疑 1 补充 3
质疑质疑论文对 TLA+ 简洁性和定位的说法，认为其缺乏真正的未来路线图
「TLA+ 的一个主要目标是简洁」——TLA+ 真的简单吗？我很难接受这一点。「TLA+ 不是编程语言，它是数学」——但数学不可执行，而 TLA+ 可以。「TLA+ 比编程语言更适合它的用途」——『对系统行为的规约』听起来就像一门编程语言，甚至是系统编程语言。总之 TLA+ 似乎没有未来：如果真有未来，本文应该更清晰地列出目标或路线图，而实际内容更像是『一切都好，无需改动』，尽管这门语言在 TIOBE 排行榜上根本不见踪影。
Mathnerd314查看英文原文
> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a programming language to me. A systems programming language, even. All this is to say that it seems TLA+ really has no future. If there was a future, like a goal or a roadmap or something, it would be outlined in this document a lot more clearly - whereas, instead, it is more like "nope, everything's good, no changes needed", even as the language appears nowhere on the TIOBE rankings.
补充资深用户认为 TLA+ 语义优秀但语法晦涩，呼吁引入 Mathlib 式的定理库和更友好的语法
我最近用 Lean 用得比较多，我最希望 TLA+ 未来能拥有类似 Mathlib 的东西。Lean 体验的妙处在于可以直接取用现成的定理，或借鉴其证明方式。我爱 TLA+，用了十年，也非常尊敬 Lamport 和 Chris Newcombe，但我觉得他们漏掉了重要的东西：TLA+ 的语义对广泛的系统工作都是很好的选择，但语法相当晦涩复杂，加大了学习难度，也难以把其他数学表达方式转换过来。我希望有人能设计一门语义与 TLA+ 相同、同样追求数学化外观、但语法更平易近人的新语言。如果有合适的库和语法，写 TLA+ 规约应该不比写 P 程序难，但我们现在还没到那一步。
mjb查看英文原文
I may have been spending too much time with Lean recently, but the number one thing I’d like to see for the future of TLA+ is an equivalent of Mathlib (https://github.com/leanprover-community/mathlib4). What’s so great about the experience of using Lean is that I can pull theorems off the shelf from Mathlib, use them if I want to, or learn from the way their proofs work if I want to do something similar. > The reason for using TLA+ is that it isn’t a programming language; it’s mathematics. I love TLA+, I’ve used it for a decade and reach for it often. I have a huge amount of respect for Leslie Lamport and Chris Newcombe. But I think they’re missing something major here. The sematics of TLA+ are, in my mind, a great set of choices for a whole wide range of systems work. The syntax, on the other hand, is fairly obscure and complex, and makes it harder to learn the language (and, in particular, translate other ways of expressing mathematics into TLA+). I would love to see somebody who thinks deeply about PL syntax to make another language with the same semantics as TLA+, the same goals of looking like mathematics, but more familiar syntax. I don’t know what that would look like, but I’d love to see it. It seems like with the right library (see my mathlib point) and syntax, writing a TLA+ program should be no harder than writing a P program for the same behavior, but that’s not where we are right now. > The errors [types] catch are almost always quickly found by model checking. This hasn’t been my experience, and in fact a lot of the TLA+ programs I see contain partial implementations of arbitrary type checkers. I don’t think TLA+ needs a type system like Coq’s or Lean’s or Haskell’s, but I do think that some level of type enforcement would help avoid whole classes of common specification bugs (or even auto-generation of a type checking specification, which may be the way to go). > [A Coq-like type system] would put TLA+ beyond the ability of so many potential users that no proposal to add them should be taken seriously. I do think this is right, though. > This may turn out to be unnecessary if provers become smarter, which should be possible with the use of AI. Almost definitely will. This just seems like a no-brainer to bet on at this stage. See AlphaProof, moogle.ai, and many other similar examples. > A Unicode representation that can be automatically converted to the ascii version is the best alternative for now. Yes, please! Lean has a unicode representation, along with a nice UI for adding the Unicode operators in VSCode, and it’s awesome. The ASCII encoding is still something I trip over in TLA+, even after a decade of using it.
补充推荐 Quint 作为 TLA+ 的替代语言
一个大家可能会感兴趣的 TLA+ 替代品：https://quint-lang.org/
threatofrain查看英文原文
A TLA+ alternative people might find curious. https://quint-lang.org/
补充询问论文 PDF 中脚注返回链接的 LaTeX 实现方式
用什么 LaTeX 宏包可以做出像链接 PDF 中那样脚注末尾带『返回』链接的效果？
bokumo查看英文原文
What LaTeX package does one use to get the "back" link at the end of footnotes like the linked PDF exhibits?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2024Hacker News 讨论帖195 分 · 105 评
同领域还值得读
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 分钟编辑精选