编程语言理论存在公共关系问题

编程语言理论（PLT）是我最喜欢的计算机科学领域之一，但我觉得它是最被外界误解的领域之一。

它充满了优美的结构和伟大的想法，将纯理论与实际应用融为一体。然而，在PLT社区之外，它却被认为是神秘的、难的、无用的、不实用的。它的问题与公众对纯数学的认知类似（“我为什么要学它？”，“它有什么实际应用吗？”），甚至更糟。

它是怎么发生的？

问题 1：理论与应用

PLT 可以作为一门纯数学学科来学习和欣赏，就像一个用来证明复杂拓扑定理的精美构造，或者一幅令人叹为观止的画作。它是一门艺术。要充分欣赏它，你需要一些教育。

一篇纯理论性的工作有时会被描述为具有“实际应用”。有时作者的意思是“它可以用于证明其他定理，并且其他8位对此主题感兴趣的人可能会发现它在实际应用中很有用”。有时，这只是对未来潜在应用的一种夸张的期望。

想象一下，一位经验丰富的软件工程师对PLT产生了兴趣，并想了解更多。有人告诉他们，应该先读读Barendregt的《Lambda演算：语法和语义》。他们费力地钻研着不熟悉的符号，努力汲取与自身经验相关的一丝洞见。最终，他们理解了Church-Rosser定理。

“Church-Rosser定理有什么用？”软件工程师问道。哦，你看，它有实际应用，只是你还不够了解而已。

工程师消失了。他的时间最好用来学习一个新的 JavaScript 框架——至少他能看到实际的好处。

即使听起来简单的定理也需要复杂的机器。尽管我们从20世纪30年代就开始了，但这些机器至今仍在建造中。

这与其他数学分支有何不同？如果你看看本科或研究生的数学课程，你会发现大多数学科都相互联系，相互依存。或者有一些著名的“桥梁”定理，提供了一种将一个数学分支的结果转化为另一个数学分支的方法。

在 PLT 中则不然。每一次开发、每一个证明都几乎是从零开始。你不会发现很多作者重复使用别人的引理和定理。甚至定义也未必一致。所以每篇论文都感觉像是从零开始。

别误会，PLT 的研究人员会互相阅读论文，并且确实会影响彼此的工作。但这种影响发生在技术和方法层面，而非形式上的重复利用。PLT 的研究人员不像其他数学领域那样，一层层地构建定理，而是倾向于根据自己的基础构造，调整和修改彼此的证明方法。

我提到过，每篇论文、每个问题都可能需要单独的设置，并有各自的定义、引理和定理。如果我们能将常见的证明技巧打包成现成的定理，并在多个证明中重复使用它们，那岂不是很好？

这当然很好，但代价是极高的抽象层级。可以把它想象成一个使用复杂架构模式、大量间接调用和多层级的代码库。它并非像意大利面条式代码那样，所有一切都是必需的，并且使用起来也很好——但学习起来难度很高。

就像那个代码库一样，从头实现每个功能会容易得多，而无需使用那么多抽象，使用抽象方法的证明也是如此。它们功能强大，但会失去直观的清晰度，并使新人难以上手。

PLT 非常难。对语言的微小改动可能会破坏你所依赖的属性，语言特性也无法很好地组合。设计空间巨大，探索每一个角落都很昂贵（世界上有多少个生产级编译器？），而我们的时间有限。

另一方面，PLT 关注的是具体的对象：编程语言。我可以用它来做实验，可以编写解释器，可以创建自己的玩具语言。很多人都这么做！为什么不也学点理论呢？这能有多难？

这是一个令人不快的意外。

我无法规定人们该做什么、不该做什么。但我完全有权写下一份愿望清单：

愿我拥有坚强的意志和清晰的思路，通过我的努力，将PLT的美好带给更多人。愿读者理解我的意图，原谅我的讽刺，并享受我的文字。