编程语言与编译

这门学科二十年里做成了一件几十年没做成的事：把内存安全从「靠程序员小心」变成了「靠类型系统保证」，而且不牺牲性能。所有权与借用检查的工业化，是编程语言理论近三十年最成功的一次落地——它的成功程度足以让多国政府在这十年把内存安全写进网络安全政策文件。与之并行的是两条同样深刻的线：形式验证从玩具规模走到了操作系统内核与编译器，而编译器从「一种语言到一种机器」变成了一个多层中间表示的生态。下面二十条按此排列：先是类型与安全，再是验证，然后是编译与合成。

一、所有权与借用检查Ownership and Borrow Checking

内存安全长期只有两条路：手工管理（快但易错）或垃圾回收（安全但有运行时代价与不可预测的停顿）。所有权系统给出第三条：每块内存在任一时刻有唯一的所有者，借用必须遵守「多个只读或一个可写」的规则，生命周期由编译器推断并检查。违反规则的程序无法通过编译，而通过编译的程序不需要运行时检查。

它的理论来源清晰——线性逻辑、区域推断与别名控制，都是学术界研究了二十余年的题目。真正的贡献是工程上的：把这些概念简化到普通工程师可以学会、把错误信息做到可读、并保证与现有生态的互操作。这是一次典型的「理论早已就绪，缺的是可用性设计」。

实测效果被多方独立确认：在采用该语言重写的大型系统中，内存安全类漏洞基本消失，而这类漏洞历来占据严重漏洞的大部分。这使它从语言偏好问题变成了安全工程问题。

代价同样明确：学习曲线陡峭、某些数据结构（图、双向链表）难以表达而需要不安全代码逃生舱、编译时间长。而「不安全代码块」的存在意味着安全保证是模块化的而非全局的——其正确性依赖于人对这些块的审查，这正是下一条要处理的问题。

它还改变了「安全」在语言比较中的地位：此前安全性被视为与性能对立的取舍，而这里两者同时达成。一旦证明取舍不存在，继续选择不安全的一方就需要新的理由——这正是它能进入政策文件的逻辑前提。

二、分离逻辑与 IrisSeparation Logic and Iris

验证操作堆内存的程序，难点在于别名：改动一处可能影响任何地方，因而推理无法局部化。分离逻辑引入一个「分离合取」——断言两块内存互不重叠，从而允许对各部分独立推理再合并。这一个连接词解决了程序验证几十年的核心障碍。

并发进一步复杂化：多线程共享状态时，所有权需要在线程间转移。这十年的成果是一套高阶并发分离逻辑框架，它把不变式、幽灵状态与所有权转移统一在一个可在证明助手中机械检查的体系里，并被用于验证真实的并发数据结构与语言语义。

最具代表性的应用是对上一条所有权语言类型系统的形式化：证明了其类型系统确实保证内存与线程安全，并给出了一套验证不安全代码块的方法——只要该块满足给定的规范，它就可以安全地被安全代码使用。这补上了前一条的缺口。

限制在于人力成本：这类验证仍需专家手工编写证明，规模以人月计。因而它的现实定位是验证关键库与语言核心，而不是验证应用程序——把信任集中到少数被严格验证的基础组件上。

值得记的是这条线与工业的关系：分离逻辑二十年间几乎没有直接用户，却在此刻成为验证主流语言核心的唯一可用工具。基础理论的价值往往在它被提出十几年后、由一个当时不存在的应用兑现。

三、验证编译器Verified Compilers

对源程序做了形式验证之后，仍有一个漏洞：编译器可能引入错误。验证编译器把这一环补上——用证明助手证明生成的机器码与源程序语义等价（在给定的语义模型下）。这类编译器已被用于航空与核电等高保障领域。

它的价值被一次独立实验清楚地展示：一项用随机测试大规模搜索编译器缺陷的研究，在主流编译器中找出了数百个错误，而在验证编译器的被验证部分中一个也没有找到。这是关于形式验证有效性的少见的经验证据。

代价是性能与覆盖：验证编译器的优化程度长期落后于主流编译器，且只覆盖语言的一个子集。这十年的进展主要在缩小这两个差距——更多优化被验证、更多语言特性被纳入。

更一般的模式是信任的转移而非消除：验证把信任从「编译器实现」转移到「语义模型与证明助手内核」。这两者更小、更稳定、更多人审查，因而是更好的信任落点。这一模式在整个形式方法领域通用。

还有一层常被忽略：验证编译器的存在，也使未验证编译器的缺陷变得可测量——有了参照系，才知道通常的缺陷率是多少。一个高标准实现的最大外部价值，有时是提供了基线。

四、代数效应与效应系统Algebraic Effects and Effect Systems

异常、可变状态、输入输出、协程、异步——这些看似不同的语言特性，在理论上可以统一为「计算发出一个效应请求，由某个处理器接管」。代数效应把这一模式做成语言原语：程序声明它可能产生哪些效应，而处理器决定如何响应。

工程收益是具体的：同一段代码可以在不同处理器下同步或异步执行、可以被测试时替换为模拟实现、可以被暂停与恢复。这解决了「函数颜色」问题——异步与同步函数不必分裂成两套 API。主流函数式语言在这十年已加入运行时支持。

效应系统的另一半是类型追踪：把「这个函数会读文件」写进类型，从而可以静态判断纯度、并发安全与资源使用。这使得能力安全（只能做被显式授予的事）可以在语言层实现，而不依赖操作系统。

推广的障碍是概念负担与类型标注的繁琐：完整的效应类型会让签名变得冗长。当前的实践取向是「运行时先行、类型系统渐进」——先提供效应处理能力，再逐步加入静态检查，与渐进类型的策略相同。

从库设计看，它解决了一个长期困扰：异步与同步版本的接口分裂使生态被迫维护两套代码。「函数颜色」问题是纯粹由语言机制造成的成本，而它的消除说明一部分工程复杂度其实源于语言设计而非问题本身。

五、渐进类型Gradual Typing

动态类型语言开发快而维护难，静态类型反之。渐进类型给出中间路径：类型标注是可选的，未标注处按动态处理，标注处静态检查，两者交界处插入运行时检查以保证类型不被违背。理论上的核心结果是「渐进保证」——增加标注不应改变已有程序的行为。

工业实践的规模远超预期：主流动态语言几乎都出现了带类型的方言或类型检查器，大型代码库以年为周期逐步标注。这是编程语言研究中理论概念被工业采纳最快的一例。

但实践偏离了理论：为避免运行时开销，多数工业实现擦除类型而不做边界检查，因而不提供理论所承诺的安全保证——类型只是文档与工具支持。学术界对此的评价是分裂的：一方认为这背叛了核心思想，一方认为这正是它能被采纳的原因。

性能问题在有检查的实现中是真实的：边界检查在混合代码中可能造成数量级的开销，若干研究专门刻画了这一「渐进类型的性能悬崖」。如何在保留保证的同时消除开销，是这条线的核心未解问题。

理论与实践的这处分歧值得单列：工业采纳了概念而丢弃了保证。这在技术史上并不罕见，但它使学术评价与工业评价指向相反的方向——学界认为有检查的实现才是正统，工业认为无检查的实现才可用。

六、内存安全的政策化Memory Safety Becomes Policy

长期以来，用哪种语言是工程团队的技术偏好。这十年的转变是：多国安全机构公开统计显示，严重漏洞中的大多数属于内存安全类，并据此发布文件要求关键基础设施软件制定向内存安全语言迁移的计划。语言选择由此成为受监管的对象。

支撑这一转变的是可核查的数据：大型代码库的漏洞分类统计一致显示内存安全类占多数，且新代码用安全语言编写后，该类漏洞随代码年龄结构变化而快速下降——「只需新代码用安全语言」这一渐进策略被证明有效，不必重写既有系统。

反对意见集中在成本与生态：重写成本高、嵌入式与实时领域的工具链不成熟、人才供给不足。折中方案是分层——在攻击面最大的组件（解析器、网络栈、媒体解码）优先替换。

更一般的意义在于责任分配：若一类漏洞在技术上可以被系统性消除，那么继续使用不安全语言就从技术选择变成了可归责的决定。这一逻辑正在通过采购要求与责任规则进入软件市场，其后果将在下一个十年显现。

从证据角度看，支撑这一政策转向的统计有其局限：漏洞分类依赖报告者的归类，而内存安全类漏洞更易被自动化工具发现，因而可能被系统性高估。这一质疑已被提出，但即便打折，结论方向不变。

七、语言的内存模型Language-Level Memory Models

在多核处理器上，编译器与硬件都会重排内存访问，因而「另一个线程能看到什么」并非显然。语言内存模型给出契约：程序员遵守数据竞争自由的规则，则可获得顺序一致的语义保证；否则行为未定义。这使得可移植的并发编程成为可能。

十余年的形式化研究发现了模型本身的缺陷，其中最著名的是「凭空出现」问题：现有的宽松模型在数学上允许一些荒谬的执行结果，而实际硬件不会产生它们。修补这一缺陷的努力持续至今，多个候选模型被提出并被形式化验证。

配套的成果是硬件内存模型的形式化：主流指令集架构的内存模型被写成可执行的形式规范，并与语言模型对接。这使「编译器把这段代码翻译成那条指令是否合法」成为可机械判定的问题。

对工程的影响体现在工具上：数据竞争检测器、模型检查器与编译器测试工具都建立在这些形式模型之上。没有形式定义，就无法自动检测违规——这是形式语义在工业中最具体的价值。

它还揭示了一件事：并发的语义此前实际上没有定义——程序员依靠经验与硬件行为编程，而这些经验在换硬件时失效。形式模型的价值不只在验证，更在于第一次让「正确」这个词在并发语境下有确定含义。

八、网页汇编WebAssembly

它是一种紧凑、快速、可沙箱执行的字节码格式，最初为浏览器设计，随后扩展到服务端与边缘计算。技术上的亮点不是指令集本身，而是它的官方规范包含完整的形式语义与类型系统，并附有机械化的可靠性证明——这在主流工业标准中是第一次。

带来的实际收益是可验证的沙箱性质：内存被限制在线性区域内、控制流受结构化约束、没有原生指针，使其隔离性可以被论证而不只是被测试。这使它成为插件、无服务器函数与不可信代码执行的通用载体。

此后的演进在补齐能力：垃圾回收支持（使高级语言可以高效编译到它）、多线程、异常、组件模型与接口类型。每一步都要在能力与可验证的隔离性之间权衡，而规范的形式化使这些权衡可以被精确讨论。

它的另一层意义是脱离浏览器之后的定位：与容器相比，它启动更快、体积更小、隔离粒度更细。「用语言级沙箱替代操作系统级隔离」是这十年系统设计中的一个真实转向，其安全性依赖于实现的正确性，而形式规范正是为此准备的。

从生态看，它的成功还有一条不常被提及的原因：它没有试图取代任何语言，而是成为一个编译目标。定位为中间层而非竞争者，使它得以避开语言之争而被普遍采纳——这一策略值得任何新平台参考。

九、多层中间表示MLIR and Compiler Infrastructure

传统编译器有一个统一的中间表示，高层信息在降级过程中丢失。多层中间表示允许在同一框架内定义多种「方言」——从张量运算、循环嵌套到硬件指令——并逐级降级，使得每一层的优化都能在拥有足够语义信息的层次上进行。

它的直接推动力是机器学习编译：从计算图到加速器指令的路径涉及若干抽象层，此前每家厂商各建一套。共享基础设施使得优化可复用、后端可插拔，大幅降低了新硬件的软件适配成本。

更广的影响是「编译器」这一概念的扩展：数据库查询优化、硬件综合、数值计算领域特定语言都开始使用同一套基础设施。编译不再专属于通用编程语言，而成为一种通用的程序变换工程。

风险是复杂度与集中化：框架本身的规模与学习成本很高，且生态高度依赖少数几家主导者。基础设施的共享既降低了每个人的成本，也把整个领域的技术路径绑定到一个实现上。

它带来的一个隐性风险是抽象层的堆积：多层方言意味着调试与性能分析必须跨层进行，而工具链的成熟度远落后于框架本身。「在哪一层出的问题」正在成为编译工程中最费时的诊断工作。

十、张量与领域特定编译器Tensor and Domain-Specific Compilers

高性能数值代码的性能取决于循环顺序、分块、向量化与并行化的组合，手工调优既费力又不可移植。这条线的核心思想是把算法（数学定义）与调度（执行策略）分离，使同一算法可以在不同硬件上生成不同的高效代码。

第二步是自动化调度搜索：用代价模型与机器学习引导，在巨大的调度空间中搜索，其结果在多个后端上达到或超过手工优化的库。「编译器通过搜索而非规则达到最优」成为这一支的标准做法，与算法面板的机器辅助发现同源。

它对硬件生态的意义重大：新加速器的可用性此前取决于厂商能否提供完整的手工优化算子库，而自动生成把这一成本大幅降低。编译器因而成为硬件竞争的关键环节，见操作系统与体系结构面板。

剩余的困难是动态形状与稀疏结构：搜索出的调度依赖于固定的张量尺寸，而实际负载（可变长度的序列、稀疏矩阵）会使预编译的最优调度失效。这正是大模型推理场景带来的新压力。

把它与算法面板的机器辅助发现放在一起看，会显出一个共同模式：当搜索空间明确且评价函数可计算时，搜索普遍胜过人工规则。差别只在于代价模型是否可靠——在编译中它是硬件性能，相对可测，因而这条线比多数同类尝试更成功。

十一、均衡饱和与电子图Equality Saturation and E-Graphs

编译器优化通常是一串按顺序应用的重写，其结果依赖顺序——先做这个优化可能挡住那个优化，这被称为「阶段排序问题」，困扰编译器设计几十年。均衡饱和用一种数据结构紧凑地表示所有等价的程序形式，反复应用规则直到饱和，最后再按代价函数提取最优版本。

关键的使能技术是电子图——一种把等价类与项结构合并存储的结构，使指数多的等价形式可以在多项式空间内表示。这十年出现的通用开源实现，使这一技术从专用工具变成可复用组件。

应用已扩展到编译优化、张量图重写、硬件综合、符号计算与程序合成。共同的模式是：把「按什么顺序变换」这一难题，换成「搜索空间的紧凑表示加一次全局选择」。

限制是饱和不总是可达（规则集可能产生无限增长）与代价模型的选择。把优化目标写成一个可计算的代价函数，本身就是一个需要判断的设计问题——这与生成设计、算法搜索面临的是同一个问题。

它对编译器的组织方式也有含义：优化不再是一串按顺序的遍，而是一个规则库加一次全局求解。这使得「加入一条新优化规则」不再需要考虑它与既有遍的顺序关系，从而降低了编译器演进的耦合成本。

十二、程序合成Program Synthesis

合成的经典形态是从示例出发：用户给出若干输入输出对，系统在受限的领域特定语言中搜索满足全部示例的最短程序。这一技术在电子表格的字符串处理中大规模落地，是形式方法少见的消费级应用。

此后二十年的技术主线是约束求解与枚举搜索的结合：把程序空间的约束交给可满足性模理论求解器，用类型与语法限制剪枝，用反例引导的归纳合成迭代收敛。规模从几行扩展到几十行。

语言模型的加入改变了格局：模型可以直接生成候选程序，而合成技术提供验证与修复——用测试、类型检查或形式规范筛选候选。这一分工被证明比任何一方单独使用都强，因为生成不可靠而验证可靠。

根本的未解问题是规范：写出精确的规范常常与写出程序一样难。示例不完整、自然语言歧义、而形式规范需要专业能力。这使合成的适用范围仍集中在规范便宜的场景——数据变换、配置、以及有强类型约束的胶水代码。

从这条线还能提炼一条通则：凡是「意图易表达而实现难」的领域，合成就有价值；凡是意图本身难表达的领域，合成只是把难题换了位置。判断一个合成应用是否有前途，先问规范从哪里来。

十三、轻量级形式方法Lightweight Formal Methods

完整验证一个大型系统成本过高。轻量路线换了目标：用规范语言描述协议与设计层面的状态机，用模型检查器穷举其状态空间，从而在编码之前发现设计缺陷。公开的工业报告显示这一做法在分布式存储与一致性协议中发现了大量人工评审无法发现的深层缺陷。

为什么有效有一个清晰解释：分布式系统的严重缺陷通常来自罕见的事件交错，而人的直觉在这类组合上系统性失效，穷举则不会。它替代的不是测试，而是「资深工程师的判断」。

推广的关键是成本：规范只覆盖设计而非实现，因而工作量以人周而非人年计；且不要求团队具备定理证明能力。这十年出现的一批更贴近程序员习惯的规范语言与运行时检查工具，进一步降低了门槛。

已知的缺口是设计与实现的一致性：验证过的设计仍可能被错误实现。把规范与代码通过运行时检查或一致性测试绑起来，是当前的主要方向，也是这条线与全程序验证之间的中间地带。

这条线的推广经验值得记：它之所以能进入工业，是因为把形式方法的收益与成本都控制在项目可承受的范围内。「不完整但便宜」的方法击败了「完整但昂贵」的方法——这在方法学的传播史上是常态而非例外。

十四、依赖类型的工业化Dependent Types, Industrialized

依赖类型允许类型依赖于值——例如「长度为 n 的数组」或「已排序的列表」，因而任意规范都可以写成类型，程序通过类型检查即证明了它满足规范。理论早已成熟，这十年的变化是可用性：更好的推断、更强的自动化策略、以及可管理的库生态。

两类应用同时成熟：软件侧是验证编译器、内核与密码学实现；数学侧是形式化数学库的建设，其规模已达到覆盖本科与部分研究生课程的水平（见数理逻辑面板）。两者共享同一批工具，互相推动。

关键的工程经验是分层：全程序依赖类型化成本过高，实际做法是把强规范用在核心不变式上，其余部分用普通类型。验证是一种可以按比例投入的活动，而不是全有或全无——这一认识使它进入了工业。

语言模型的介入是当前最活跃的方向：用模型生成证明脚本，由内核检查其正确性。这是生成式技术与形式方法的天然配对——生成不可靠而检查可靠，因而错误不会通过。其效果已在数学形式化中被验证，在软件验证中刚开始。

它与数学形式化的互相带动值得单列：软件验证需要的库与数学形式化需要的库大量重合，而后者吸引了大量数学家参与，反过来提高了工具的成熟度。两个本不相干的社群共用一套基础设施，是这十年的一次意外收获。

十五、增量与响应式计算Incremental and Reactive Computation

许多程序反复在略有变化的输入上运行——编译、界面渲染、数据管道、增量查询。手工实现增量更新既易错又难维护。这条线的思想是让运行时记录计算的依赖图，输入变化时只重算受影响的节点。

它的理论形态是自调整计算与增量计算的复杂度分析：给出「输入变化的规模」与「重算代价」之间的关系，从而可以证明某些算法的增量版本代价与变化量成正比而与总规模无关。

工业落地相当广泛：现代构建系统的缓存与增量编译、界面框架的重渲染最小化、流式数据库的增量视图维护，用的都是同一套依赖追踪思想。它是本面板中理论到实践距离最短的一条。

剩余的难点是缓存的正确性与规模：依赖图本身可能巨大，且任何未被记录的隐式依赖（环境变量、时间、文件系统状态）都会造成错误的复用。「可复现构建」正是为了消除这类隐式依赖，两条线因此绑定在一起。

从它可以看出「隐式依赖」是软件工程中最普遍的错误来源之一：任何未被记录进依赖图的输入，都会在缓存复用时变成难以复现的缺陷。可复现构建与增量计算因此是同一个问题的两面。

十六、并发编程模型的收敛Convergence of Concurrency Models

回调、期约、协程、通道、参与者——并发模型多年并存且互不兼容，其共同问题是任务的生命周期与错误传播缺乏结构：启动的任务可能泄漏，异常可能无处可去，取消操作难以正确实现。

结构化并发的原则是：任何并发任务都必须在某个作用域内启动，作用域退出前所有子任务必须完成或被取消，错误沿作用域向上传播——与结构化程序设计对控制流做的事情完全类似。多种主流语言在这十年采纳了这一原则。

它与效应系统、与所有权都相互配合：所有权保证共享数据的安全，效应系统追踪并发效应，结构化并发保证任务生命周期。三者合起来，才使「并发默认安全」成为可能。

取消与超时仍是最难的一环：正确的取消需要每一层都能被中断并清理资源，而现有的库生态大量代码不具备这一性质。一个语言特性的价值，最终由生态是否配合决定。

这一条还提供了一个语言演进的通用观察：新特性的实际效果取决于既有生态是否配合。结构化并发在新代码中效果良好，而与旧库交界处仍会泄漏——这决定了它的收益要以年为单位、随生态更新而缓慢兑现。

十七、超优化与自动向量化Superoptimization and Auto-Vectorization

传统编译器优化由人编写的重写规则组成，规则的正确性靠评审与测试。超优化换了路径：在给定指令集上穷举或求解搜索出与原片段等价且更短的指令序列，并用求解器证明等价。它既能发现人未想到的优化，也能自动验证优化的正确性。

工业价值最明显的场景是密码学与位运算密集的代码，以及为新指令集扩展快速生成优化规则。同类技术还被用于发现编译器中已有优化规则的错误——把规则本身作为待验证对象。

自动向量化是长期难题：把标量循环转成宽向量指令，需要判断依赖、对齐与掩码，编译器的成功率长期不稳定，程序员因而依赖手写内建函数。近年的进展是把向量化表述为搜索加验证问题，成功率有实质提升。

限制是规模：求解器只能处理短片段，因而这类技术用于「窥孔」而非全局优化。它的定位是把人写规则的工作自动化，而不是替代整个编译流程。

它的另一个用途值得强调：把编译器自身的优化规则当作被验证对象。这类「用形式方法检查工具链」的做法，比验证应用程序的性价比高得多，因为一处修正惠及所有使用者。

十八、概率与可微编程Probabilistic and Differentiable Programming

概率编程让程序员写出生成模型，由语言运行时负责推断——蒙特卡洛采样或变分方法。其价值在于把建模与推断分离：模型可读、可修改，而推断算法可替换。这与张量编译器把算法与调度分离是同构的设计思想。

可微编程的问题类似：自动微分从库函数上升为语言特性，涉及控制流、可变状态与高阶函数的求导语义。形式化「对一个带循环和分支的程序求导意味着什么」并非平凡，这十年的工作给出了若干严格的语义与正确性证明。

两条线的共同技术挑战是效率与可组合性：通用推断算法在复杂模型上收敛慢，通用自动微分在稀疏与离散结构上开销大。因而实践中仍需针对模型族特化，这削弱了「通用语言」的承诺。

更值得记的是它们对语言研究的启发：当一个计算范式足够重要，它会从库上升为语言特性，从而获得类型检查、优化与形式语义。这一过程在垃圾回收、并发与异常上都发生过，如今轮到了推断与求导。

还有一点值得记：这两条线都始于「让研究者写得更方便」，最终却改变了什么模型可以被研究——工具决定了可探索的空间。这与科学仪器对学科的作用完全同型。

十九、语言生态与包管理的安全Ecosystems, Package Managers and Supply Chain

现代程序的绝大部分代码来自依赖。这十年的多次事件——某个微小包被删除导致大范围构建失败、维护者账户被接管注入恶意代码、以及广泛使用的压缩库被长期渗透——把包管理从工程细节推到了安全核心。

语言层面的回应包括：可复现构建（同样的源码产生逐位相同的产物，从而可被独立验证）、锁文件与最小版本选择、以及对构建脚本执行权限的限制。这些都是语言与工具链的设计选择，而非应用开发者能自行解决的问题。

更深的问题是信任的传递性：使用一个包等于信任其全部依赖及其维护者。已有的应对是能力限制（依赖默认不能访问文件与网络）与沙箱化执行，而这要求语言具备细粒度的能力控制——与效应系统直接相关。

结构性困难在于激励：维护者多为无偿劳动，而使用者是营利机构。安全事件的根源常常是维护者精力枯竭而非技术缺陷，因而技术手段只能缓解，不能解决。

从制度上看，这条线暴露的是公共品的供给失败：关键依赖是全球基础设施，其维护却依赖个人的业余时间。已有的资助计划规模远小于风险规模，而这一失衡在下一次重大事件前很难被纠正。

二十、语言模型进入编程语言研究Language Models Meet PL Research

模型生成代码的正确率有限，但类型检查器、测试、静态分析与定理证明器都是可靠的判定器。由此形成一个稳定的模式：用模型提出候选，用形式工具筛选。在有强规范的场景（类型丰富的语言、有测试的项目、可形式化的定理），这一组合的效果远好于单纯生成。

第二个方向是把模型用于此前无法自动化的环节：从代码推断可能的规范与不变式、生成证明脚本、解释类型错误、以及在重构中维持语义。这些任务的共同点是「猜测部分」难而「验证部分」有现成工具。

对语言设计的反向影响正在出现：如果大量代码由模型生成，那么语言应当优化为「易于验证」而非「易于书写」——更强的类型、更明确的效应、更严格的默认值。这与过去二十年追求简洁语法的方向部分相反。

尚无定论的是长期后果：若生成成本趋近于零，代码的复用与抽象的价值可能下降，而可读性与可验证性的价值上升。这一判断已被提出，但没有足够的经验证据支持——它将由下一个十年的工程实践来裁定。

最后补一句判断上的谨慎：目前关于生成式工具对代码质量长期影响的证据仍很薄弱，且多为短期研究。本条列出的是方向性推论而非已确立的事实——真正的检验要等到大量模型生成的代码进入长期维护阶段。

二十条排在一起，这门学科二十年最大的成就是把一批「原则上正确」的理论做成了「工程上可用」的东西。所有权类型、分离逻辑、依赖类型、代数效应、渐进类型——五者的理论都在二十世纪末就基本就绪，真正花掉这二十年的是可用性：错误信息、推断能力、生态互操作、学习曲线。这提示一条对整个计算机科学有效的经验：理论与实践之间的障碍常常不是正确性，而是人机工程。

第二条主线是信任的重新分配。验证编译器把信任从编译器实现移到语义模型与证明内核，形式化的字节码规范把隔离性从测试移到证明，轻量级形式方法把设计正确性从资深工程师的判断移到穷举检查，而内存安全的政策化把语言选择从技术偏好移到可归责的决定。每一次移动都遵循同一原则：把信任集中到更小、更稳定、更多人审查的组件上，而不是试图消除信任。

第三条主线刚刚开始：当代码越来越多由模型生成，这门学科的价值主张发生了反转。过去它的核心竞争力是帮助人写出正确的程序；现在它最稀缺的能力是判断一段来路不明的程序是否正确——而类型系统、静态分析、模型检查、定理证明恰好都是判定器。生成不可靠而检验可靠，这一不对称性使得编程语言研究从「写作的辅助」变成了「验收的基础设施」。若这一判断成立，那么语言设计的取向也会随之改变：从易于书写转向易于验证，而这与过去二十年的主流方向恰好相反。