我与 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 当年的观点并未完全站住脚。这段经历让我见证了学术争论的复杂与类型演进的必然。