编程语言探索的时代已然到来

# 编程语言探索的时代已经到来。 来源：https://kirancodes.me/posts/log-end-of-pl.html ## PL 研究已死，PL 探索的时代才刚刚开始\! 02 Oct, 2026programming\_languagesresearchperspectives 最近 TYPES 邮件列表上有一场讨论，研究者们就 AI 工具对编程领域的颠覆性影响，推测着我们这个领域的未来。 讨论中的观点纷繁多样。有些看法是积极的，但主流意见压倒性地偏向悲观。说一些研究者此刻正面临着生存危机，似乎也并不夸张： > 我从旁观者的角度观察到，许多学界人士在 2026 年秋季对工作的感受比一年前更糟 ...\.*士气和动力双双下滑*，压力与焦虑水平上升，相应的心理健康风险也在增加。其影响堪比**COVID 时期**。 我想借这篇文章提出一个不同的立场。我知道此刻许多初入行的研究者正在关注这场讨论，学生们面对在动荡时代规划职业前途的艰巨任务而深感茫然，纠结于在这个气候下是否还有必要进入 PL 领域。我想为他们描绘一幅稍微积极一些的图景。 坦白说，作为一名研究者，我**从未如此兴奋过\!**研究灵感的源泉从未如此充沛，新问题每天都在涌现，而我提出和回答问题的速度远超以往。 本文的核心观点是：作为整个社区，我们需要从那种由自我驱动的、把研究工作当作某种"努力"或"聪明"的证明来捍卫的立场，转向那个一直应当作为我们根基的、更真实也更高尚的动机——转向**探索\!** ### 编程语言已死。那又怎样？谁在乎？ 让我们深入探究一线研究者们的恐惧，并列出以下几点： - 大语言模型在编写代码方面极为出色。 - 因此，人类将越来越少地亲自动手写代码。 基于此，研究者们担心自己的研究正在变得过时，是可以理解的。人类将不再编写程序。那又何必关心编程语言呢？反正人类也不再需要去写它们了。 **那又怎样？** 编程语言研究自诞生以来，就一直架设在理论与应用之间的桥梁之上。作为 PL 研究者，我们得以与那些有原则的、优美的思想为伴。我们不必为了实用性而牺牲这些思想，但与此同时，我们工作的下游成果最终还是会归结到实际应用上。 但……说真的？谁在乎那些应用？我的意思是，我们本来就不喜欢应用。要是喜欢，我们早就去做软件工程了。我跟软件工程领域的研究者共事过。相信我。那场面可不怎么好看。他们的系统是临时拼凑的， hacky 的，严重残缺的，勉强能跑。但他们不得不那样。如果你想构建一个能够处理整个 Linux 内核的静态分析工具，你就不能只满足于美与优雅。 我想说的是，PL 那些美妙的思想、那些洞见、那些美，它们依然都在。它们依然触手可及，而我们完全有能力继续去探索、去把玩、去享受其中的乐趣。到底谁在乎有没有人使用编程语言呢？我来给你透露一个小秘密：绝大多数编程语言，除了它们的开发者之外，字面上一个用户都没有。 **去他妈的用户。去他妈的应用。让我们认认真真地做点 PL 研究吧\!**而如今有了大语言模型，我们可以挑战比以往任何时候都更大、更疯狂的问题\! ### 编程语言探索的新西部 我刚刚解释了为什么大语言模型以及程序员构成的变化不应削弱你对 PL 研究的热情——那些*思想*、那些*美*、那些**乐趣**，全都还在\!但现在我想告诉你，为什么大语言模型让我对 PL 研究的未来无比兴奋。 简而言之，我认为我们如今拥有了令人疯狂的智能工具，让我们能以前所**未**有的速度提出、检验和验证研究中的反事实假设。这太疯狂了。 过去几个月，我一直兴奋得近乎疯狂。每天都能撞上新的想法。 我们赖以立足的许多假设已经彻底被推翻。我们的软件生态系统建立在一个庞大的假设网络之上，而其中许多假设已不再成立。对每一个假设的质疑，都能带给我们全新的、有趣的研究方向。 - Ship your interpreters (https://github.com/BasisResearch/ship-your-interpreter/)——大语言模型极其擅长处理和管理那些繁琐枯燥的证明工作，其规模是任何人类独自完成不了的。只要把一个问题交给大语言模型，它们就能一路验证程序直到二进制层面。利用这一能力，我开展了一个实验：让大语言模型自动生成被解释语言的语义，然后证明该语义抽象了该语言具体二进制的行为。一年前，这个想法简直完全不可想象，但今天呢？今天它不过是花上一个月时间写提示词的事。 - AI-first Verified Tooling（进行中）——验证工具和语言工具链，其设计是围绕并受限于人类用户的能力。据我观察，大语言模型的长处与短处虽然与人类相似，但并不总是相同的。所以，或许可以调整工具的界面，使其更能适应智能体这种"参差不齐的智能"——比如，向工具暴露更多内部细节，例如 SMT 求解器的实例化图等等。我们正在与 Amazon 合作开展一些实验，尝试通过暴露这些细节来提升大语言模型使用此类验证工具的能力。 - 为新语言开发语义（进行中）——我所在单位的同事们开发了一种用于动力系统的新语言 dynestyx (https://arxiv.org/abs/2606.16985)。他们并非编程语言研究者，但我们帮助他们打造了一门*非常酷的*新语言，将他们领域中的大量工作统一了起来。这门语言缺少形式语义，而这正是我非常擅长协助搭建的东西，但我并非他们领域的专家，我们也没有足够的时间坐下来慢慢让我补上这一课。于是，作为一种新型的协作方式，我一直在尝试用大语言模型自动生成他们语言的机械化大步语义，通过测试加以验证，然后与他们共同迭代这一语义，使其符合他们的意图。 除了这些应用领域之外，大语言模型对理论工作同样令人兴奋。自动化证明撰写的工作量，让提出反事实假设变得轻而易举。如果我在语言中加入这个构造呢？它还是强正规化的吗？如果我这样修改类型系统呢？它还是可靠的吗？我现在能够以前所未有的速度不断迭代。 当然，我觉得在做这些了不起的事情时，自己似乎确实失去了一些需要亲自动手的"功夫"。我过去曾为自己的编程和开发能力深感自豪。我曾单枪匹马构建过数十万行代码的项目，使用的还是冷门又小众的语言。我曾为设计和证明那些深奥类型系统的性质而辛勤耕耘。我的代码是一种手艺，一种我引以为傲的手艺。但从某种意义上说，那更多是我的自我，而非我的求知欲。那些思想？那些洞见？那些探索？这些严格来说都不需要我的专业技能。 ### 再会，快乐 hack，亲爱的 PL 新人们\! **抛弃你的自我\!解放你的灵魂\!投入探索的喜悦吧。**研究从来都是探索。拓展人类知识的疆界。这就是科学之美，这就是成为科学家的意义。多提问题。深入调查。潜入深处。你现在拥有了能够让你以前所未有的方式提出问题、搜寻答案、深入探索现实深处的工具。好好利用它们。享受它们。 *让编程语言探索的时代开启吧\!* 我相信，我们正迎来一个真正具有变革意义的时刻。我无比期待我们即将踏入的那个疯狂而精彩的未来\!