编程语言与软件工程2025nickbenton.name
Coq：世界上最好的宏汇编器？
Coq: The World's Best Macro Assembler? (2013)
进阶 · 约 45 分钟读完前置知识：汇编语言基础、Coq/Rocq 基础、形式化验证概念
导读
这篇 2013 年的论文提出用 Coq（现名 Rocq）作为“宏汇编器”的思路：借助 Coq 的证明能力，在编写汇编代码的同时对其语义性质进行形式化证明，从而把汇编器变成一个可验证正确性的工具。作者认为这可能是“世界上最好的宏汇编器”。
HN 关注点：是因为形式化验证与底层编程的结合：在安全关键系统中证明汇编代码语义正确性极具吸引力，讨论焦点是这种方法的现实可行性与 Coq/Rocq 是否仍是合适工具。
HN 评论精选
这几条评论里：支持 1 质疑 1 补充 2
支持安全关键系统从业者认为这是梦想工具：证明汇编语义正确性的增量成本很低，值得深入发展
发帖者：我大约每年重读一次这篇论文，它可能是我读过的最重要的论文之一。作为从事高可靠安全关键实时系统（汽车、航空电子）的人，能在一个可以证明汇编代码语义性质的环境里工作，几乎是我的梦想——证明代码正确的成本本来就远高于写代码的成本，因此转向汇编的增量成本似乎很小，只要验证正确性所需时间能有所回报。实际上，我理想中的语言是一个较丰富的宏汇编器加上一个（引导式、贪心的）寄存器分配器，完全为简化和支持语义证明而设计。我不确定 Coq（Rocq）今天是否是正确答案，或是否有更新的文献推进这一方向，但我真心希望看到让低级语言在这个领域更有用的深入研究，而不是转向更受限的更高级语言。
addaon查看英文原文
Poster here. I re-read this paper about once a year. I continue to think that it may be one of the most important papers I've read. As someone who works on high-reliability safety-critical real-time systems (automotive, avionics), being able to work in an environment where I could prove semantic properties of assembly code is pretty close to my dream -- the cost of demonstrating code correct is already so much higher than the cost of writing the code that the incremental cost of going to assembly seems minor, if there's even a small payback in time to demonstrate correctness. In practice, I think my dream language would be a relatively rich macro assembler plus a (guided, greedy) register allocator, designed entirely to simplify and allow semantic proofs. I don't really have a sense as to whether Coq (Rocq) is the right answer today, vs other options; or if there's a newer literature advancing this approach; but I'd truly love to see a deeper focus of making low level languages more useful in this space, rather than moving towards more constrained, higher level languages.
质疑认为 Lisp 同样能实现这种严谨的形式化能力
Lisp 可以轻松模仿 Prolog 以及 Coq 那样的严谨性。
anthk查看英文原文
A Lisp can mimic Prolog and the rigour of Coq with ease.
补充x86 复杂性使得强大的汇编器对防错很有必要
x86 架构和指令集非常复杂，所以绝对需要一个强大的汇编器来帮助避免错误。
asdefghyk查看英文原文
The x86 architecture and instruction set is complex - so it absolutely needs a powerful assembler to help prevent mistakes.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2025Hacker News 讨论帖167 分 · 74 评
同领域还值得读
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 分钟编辑精选