历史与人物inference-review.com编辑精选
Dijkstra：把计算机科学扛在肩上的人
Edsger Dijkstra – The Man Who Carried Computer Science on His Shoulders
2020 — 2024，它一次次回到首页
黑点是上首页（≥ 50 分）的那次投稿，空心点是没冲上去的投稿，点越大分数越高。
导读
这篇长文评传回顾了 Edsger Dijkstra 的学术生涯与思想，包括他在结构化编程、goto 有害论和程序正确性证明等方面的贡献。文章也刻画了他特立独行、不循常规的学术风格与好斗性格，并讨论其遗产的争议与影响。
为什么经久不衰：它把 Dijkstra 的技术贡献、性格争议和学术生态放在一起审视，既解释了他的思想为何奠基，也解释了为何至今仍被反复讨论。
HN 评论精选
程序正确性证明的难点常在规格本身，Dijkstra 的方法影响大但落地困难。
我在约1970年上大学时读了 Dijkstra 的《goto 语句有害论》，当时我还是年轻程序员，它让我重新思考大型程序为何常常难以理解。多年后读研时我研究程序验证，Dijkstra 对该领域影响很大；我曾参加他在去美国前于 UT Austin 做的一场讲座。Dijkstra 的程序正确性证明方法在实践中很难应用：就像几何证明一样，正确性证明本身也可能有不易察觉的错误。以排序为例，如果规格只说输出必须有序，一个被证明的程序仍可能没有正确排序；规格必须要求输出是输入的排序排列，而不是简单的有序、等长等更弱条件。真正的验证还必须处理计算机实现的奇特数学，而我们在学校习惯的数学理论假设无限精度……
todd8查看英文原文
I read Dijkstra's goto considered harmful in college, circa 1970. I was a young programmer at the time, and it made me think and reconsider how and why big programs were often hard to understand. Years later, in grad school, my research was on program verification. Dijkstra was a big influence on the field. I attended a lecture at UT Austin that he gave before moving to the US. Dijkstra's approach to proving the correctness of programs is hard to apply in practice. Like a geometry proof, there are ways in which a proof of correctness can have mistakes that aren't obvious. Here's an example, prove that a sorting algorithm works. If the specification is that the output must be in sorted order, a proven program can still fail to sort correctly. The specification has an error, the output must not only be in sorted order, it must ensure that all of the input elements make it somewhere to the output. But this isn't good enough. A sort proven to meet this specification might leave out some duplicate values. Requiring that the output be the same length as the input still isn't good enough, multiple copies of one element might hide missing duplicate input values for another element. The specification requires that the output be a sorted permutation of the input. Sorting is a well understood problem, but real verification must deal with the strange mathematics implemented by computers. The mathematical theories that we are accustomed to from school assume infinite precision and no overflow, real life hardware doesn't act this way. All of this makes program verification hard, and my hope is that AI programming assistants will someday aid in the construction of meaningful specifications and work with the programmer to verify the correctness of programs or determine their safe operating boundaries. Progress has been slow, and the tools are still impractical for use by most programmers on most programs.
他反叛现代学术指标却成就卓著，提示当前评价体系可能偏狭。
令人惊叹的是，他如此违背现代学术规范：不争取外部经费、论文相对少、很少合作、几乎没有博士生。可以说，今天一个年轻研究者若有这些特征，很可能在进入终身教职评审前就被任何美国顶尖研究型大学解雇。也许我们现代的学术评价指标漏掉了某些东西？
xenocyon查看英文原文
It is remarkable how much he contravened modern academic norms: no work to bring in external funding, relatively few papers, very little collaboration, almost no PhD students. It's not an exaggeration to say that a young researcher with these characteristics today would likely get fired from any high-ranked American research university before even coming up for tenure review. Perhaps our modern academic metrics of merit are missing something?
Dijkstra 对 BASIC 的尖刻名言常被断章取义，用来贬低现代 BASIC 语言。
我希望看到 Dijkstra 这个名字时，不要立刻想到他那句常被引用的 BASIC 评论：'实际上不可能教好那些先接触过 BASIC 的学生编程：作为潜在程序员，他们在精神上已被残害到无法再生的地步。' 问题是，人们引用这句话时不管所谈的 BASIC 方言与 Dijkstra 所指的有多相似。如今有很多优秀的 BASIC 语言运行着各种有用软件，却仅因这句话就被一部分开发者一概否定。
mysterydip查看英文原文
I wish seeing the name Dijkstra didn't immediately remind me of his oft-quoted BASIC comment: "It is practically impossible to teach good programming to students that have had a prior exposure to BASIC: as potential programmers they are mentally mutilated beyond hope of regeneration." The problem is it's quoted regardless of how much the BASIC dialect being discussed resembles the one he was talking about [1]. There are lots of good BASIC languages out there running all kinds of useful software that are dismissed out of hand by a subset of developers simply from that comment. [1] https://programmingisterrible.com/post/40132515169/dijkstra-basic
Dijkstra 贡献巨大但非唯一，正确性证明因成本高未流行；他的傲慢与坚持同样鲜明。
至少可以说，是他自认为把计算机科学扛在肩上。他做出了重大而重要的贡献，但不是唯一一个：Hoare、Backus、McCarthy……很多人都做出了重要、基础性的贡献。结构化编程流行了，正确性证明却没有，原因大概会让 Dijkstra 不快——证明费时，而快速产出大体能用的软件（无论社会还是经济上）比慢速产出被证明正确的软件更有价值。但他绝不会接受现实世界如此；他坚持自己的方法正确。正如 Backus 评价他：'这家伙的傲慢令人咋舌。' 所以：重要贡献？绝对有。比任何人都多？也许。把计算机科学扛在肩上？没有，但他大概自认为如此。
AnimalMuppet查看英文原文
Or at least who thought he carried computer science on his shoulders. He made significant, important contributions. He wasn't the only one. Hoare, Backus, McCarthy... there were a lot of people who made important, fundamental contributions. Structured programming caught on. Proofs did not, for reasons that would have offended Dijkstra - they took time, and it was actually more valuable (both socially and financially) to produce mostly-working software quickly than to produce proven-correct software slowly. But he never would have accepted that the real world was that way. He insisted that his approach was correct. As Backus said of him, "This guy’s arrogance takes your breath away." So: Important contributions? Absolutely. More than anyone else's? Perhaps. Carried computer science on his shoulders? No, but he probably thought he did.
历次讨论
同类还值得读
开发者无薪坚持完成 Mac 图形计算器：一个秘密项目的故事
Dev stays without pay to finish Mac Graphing Calculator as skunkworks project
苹果 Mac 图形计算器（Graphing Calculator）开发者的亲述：在项目被砍后，几位工程师在没有报酬、没有正式授权的情况下，以“地下项目”方式偷偷留在公司把软件做完…
历史与人物上首页 6 次 · 2009–2022pacifict.com理查德·费曼与 Connection Machine
Richard Feynman and the Connection Machine
长文回忆费曼晚年参与 Connection Machine 并行计算机项目的经历：他分析路由器、用自创的并行 Basic 编写 QCD 程序，也涉足细胞自动机等主题。
历史与人物上首页 5 次 · 2010–2021longnow.org编辑精选负 2000 行代码
-2000 Lines of Code
folklore.org 上 Andy Hertzfeld 记录的一则苹果 Macintosh 开发轶事：Bill Atkinson 被问到写了多少行代码时，回答“-2000 行…
历史与人物上首页 4 次 · 2014–2022folklore.org编辑精选Dennis Ritchie 的第一版 C 编译器（约 1972 年）
Dennis Ritchie’s first C compiler (c. 1972)
这个 GitHub 仓库保存了 Dennis Ritchie 约 1972 年编写的最早 C 编译器源码，是 C 语言和 Unix 早期历史的一手材料。
历史与人物上首页 4 次 · 2013–2025github.com一位破解赛马密码的赌徒
A Gambler Who Cracked the Horse-Racing Code (2018)
彭博社 2018 年的长篇特写，讲述数学家 Bill Benter 如何用统计模型和算法在赛马博彩中持续盈利、累计赢得近十亿美元的故事。
历史与人物上首页 4 次 · 2018–2024bloomberg.com