我与 Leslie Lamport 合写那篇论文的始末
I came to write THAT paper with Leslie Lamport
Leslie Lamport 以分布式系统和 LaTeX 闻名，他曾撰写《Types Considered Harmful》一文抨击类型系统。当我作为审稿人准备拒稿时，编辑 Andrew Appel 却提议我与他合作重写，让文章在保留原意的同时技术上更准确。我们经历了两轮审稿的波折，最终文章得以发表。27 年过去，类型系统已在 CompCert、seL4 和 Amazon Nitro Isolation Engine 等项目中证明其价值，而 Leslie 当年的观点并未完全站住脚。这段经历让我见证了学术争论的复杂与类型演进的必然。
验证是发现错误的极其昂贵的方式，而那些未被发现的错误可能让你的证明毫无价值。
HN 评论区
11- joomy
不知为何，博客文章里没有链接到那篇论文的终稿：https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> 另一位审稿人 David McAllester 也得出了同样的结论。
是那个提出 PAC-Bayesian 界限的 David McAllester 吗？
答：是的。
- mrkeen
> 这个论点确实有几分道理。1992 年写那篇笔记时，类型系统正处于动荡之中。Coq（现称 Rocq）刚刚问世，Martin-Löf 类型论也正经历重大变革。至于简单类型论，HOL 的早期实现才出现没几年。当时人们还搞不清楚任何类型化演算到底能做什么。证明助手那时还不支持类型类。John Harrison 引入他那招“低成本依赖类型”的 trick 还要等上好几年，而这一招足以很好地表达 Tn。
我并不想把线性类型或依赖类型塞进 TLA+。用穷尽运行时来证明动态属性，和你静态能做的事情完全是两码事。
但我确实想排除胡扯。当然，我可以证明交通灯永远不等于 RED_LIGHT。可惜，如果它等于 RED 呢？