算法与理论计算机2017homepages.inf.ed.ac.uk
证明即程序：19世纪逻辑与21世纪计算（2000）
Proofs are Programs – 19th Century Logic and 21st Century Computing (2000)
入门 · 约 45 分钟读完前置知识：命题逻辑基础、函数式编程初步
导读
Philip Wadler 的经典文章《Proofs are Programs》，梳理 19 世纪 Frege、Russell 等人的逻辑学如何演化为 20 世纪的计算理论，核心论点是“证明即程序、命题即类型”（Curry-Howard 对应）。文章以讲故事的方式连接逻辑史与现代函数式编程。
HN 关注点：逻辑与计算的深层联系，讨论焦点是这种“历史必然进步”叙事是否成立，以及非构造性证明如何对应程序。
后来怎么样
该文是 Curry-Howard 对应最广为流传的科普性综述之一，长期被用作函数式编程与类型论教学的入门读物
HN 评论精选
这几条评论里：支持 1 质疑 1 补充 2
质疑批评该文是计算机科学家视角的“辉格史观”，把历史写成通往现代计算观念的必然进程
人们喜欢这样看待逻辑与计算的关系，作者也是讲故事的高手。但这种视角有些误导，类似“辉格史观”——把历史描绘成通往当下正确观念的必然进步，只是把“更大的自由”换成了计算机科学家（包括作者）所主张的当今做计算机科学的正确方式。我很想读一篇由真正的历史学家（而非为自身世界观扭曲历史的计算机科学家）写的相关历史论述。
tpetricek查看英文原文
People like to see logic and computing in this way and the author is a great storyteller. But it is a somewhat misleading perspective that is kind of similar to "Whig historiography" (https://en.wikipedia.org/wiki/Whig_history): > Whig is an approach to historiography that presents the past as an inevitable progression towards ever greater liberty and enlightenment, culminating in modern forms of liberal democracy and constitutional monarchy. Just replace the "greater liberty" bit with what computer scientists (and the author) argue is the right way of doing computer science today. I'd love to read a historical treatment of the topic that is written by someone who is a historian rather than computer scientist twisting history to support their world view.
补充提问：非构造性证明（对角线法、概率方法）在“证明即程序”框架下如何对应程序
有熟悉这个主题的人吗：非构造性证明，比如康托尔对角线法或 Erdős 的概率方法，也算程序吗？它们只是不终止的程序吗？我能很容易把对角线法想象成一个不终止的程序，但不明白概率方法作为程序是什么样子。
jwtadvice查看英文原文
Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-terminating programs? I can see Cantor Diagonalization as a non-terminating program really easily, but I don't understand what the Probabilistic Method looks like as a program.
支持推荐此文，作者擅长把复杂概念讲得平易近人
我很喜欢 Wadler 的论文。他写过一篇关于 Monad 的论文，对我既平易近人又有启发性。我也热爱逻辑和谓词演算。强烈推荐这篇。
agentultra查看英文原文
I love Wadler's papers. He did one on Monads that was approachable and revealing for me. I also love logic and the predicate calculus. Highly recommend reading this one. :)
补充感慨历史上计算被局限于数值计算，符号计算的思想姗姗来迟，并追问今天我们正错过什么简单而伟大的想法
稍微跑题：我一直好奇为什么 Babbage 没有走布尔逻辑的路线做计算？为什么不用电报继电器？Hollerith 为什么也没有？似乎都受困于“计算就是数字”的定式思维——只有计算和制表。虽然 Boole 提出了逻辑数学，但很少有人造机器去实现它；用电路实现逻辑还要再等几十年。后来“计算是关于符号而非数字”的顿悟才打开了一切。事后聪明当然容易，我只是好奇我们今天正错过哪些“显而易见”的想法，以及为什么改变世界的简单想法往往要那么久才被发现。
cr0sh查看英文原文
This may be slightly OT - but the one thing I have always wondered about the 19th century is why Babbage didn't go down the route of Boolean logic/math for computation? Furthermore, why he didn't incorporate and use relays (from telegraphy)? For that matter, why didn't Hollerith? Ultimately, to me it seems all connected to this "fixed" idea (that is, thinking "inside the box") that computation was about numbers - that there was only calculation and tabulation - counting, iow. While Boole came up with the math/logic - few pursued the idea of making machines to work with it (a few -did- exist, but were obscure, iirc); embodying logic using electrical circuits would have to wait. Then there was the "revelation" of computation being about symbols, not numbers - which opened everything up. I'm just kinda rambling here; my apologies. And, hindsight is always easier than foresight, of course. It just bugs me, and makes me wonder what "obvious" ideas we are missing today, that will change the world, that we won't know until we look back. I guess I wonder why many of the most world changing ideas (in the long run) are often very simple, and why did it take so long for humanity to see/discover them? I wonder if anyone has studied this - of if it is something that can be studied...?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2017Hacker News 讨论帖152 分 · 77 评
同领域还值得读
哲学家为何应关注计算复杂性
Why Philosophers Should Care About Computational Complexity (2011)
Scott Aaronson 的这篇长文论证计算复杂性理论（如 P vs NP、停机问题的复杂度视角）对哲学问题（如知识的本质、中文房间、水槽论证等）具有实质意义，而不仅是技术细…
算法与理论计算机2015 · 552 分 · 120 评进阶 · 约 90 分钟编辑精选通信的数学理论
A Mathematical Theory of Communication
是香农1948年的《通信的数学理论》，为通信建立数学框架：把信息量定义为不确定性或自由度（信息熵），并讨论信源编码、信道容量与可靠传输。
算法与理论计算机2020 · 495 分 · 91 评进阶 · 约 120 分钟编辑精选物理、拓扑、逻辑与计算：罗塞塔石碑
Physics, Topology, Logic and Computation: A Rosetta Stone (2009)
用范畴论充当“罗塞塔石碑”，试图在量子物理、拓扑、逻辑与计算四个领域之间建立统一的结构性类比：物理中的量子过程、拓扑中的配边、逻辑中的证明和计算中的程序，都可被视为某类范畴中的态…
算法与理论计算机2009 · 390 分 · 55 评 · 引用 13专业 · 约 180 分钟编辑精选一种快速、极小内存的一致性哈希算法
A Fast, Minimal Memory, Consistent Hash Algorithm
论文给出一种快速、省内存的一致哈希方案，目标是在桶数量变化时保持较小的键迁移成本，同时降低计算和内存开销。
算法与理论计算机2014 · 327 分 · 57 评 · 引用 4进阶 · 约 25 分钟编辑精选第五个 Busy Beaver 值的确定
Determination of the fifth Busy Beaver value
宣布确定了第五个 Busy Beaver 值 BB(5)：即 5 状态图灵机中停机前运行步数最多的机器（Champion）在 47,176,870 步后停机。
算法与理论计算机2025 · 288 分 · 116 评 · 引用 1专业 · 约 75 分钟编辑精选