最后一门编程语言，也许不是给人用的

今天早上，我站在书桌前，喝着兑得很淡的速溶咖啡，做着每天早上处理完高优先级邮件和通知之后都会做的事：花三十分钟看 HackerNews。这是一个我限定时长、从不跳过的仪式。我每天都去办公室，无论是在那张书桌前还是在家里的书桌前，早晨都一样：咖啡，站姿，首页。

要把握湾区、科技与科学的脉搏，了解一夜之间冒出了哪些激发思考的想法，HackerNews 仍然是最好的途径之一。我也订阅了几份精选的新闻通讯，但这些年我发现，只要你懂得从低信号中筛出高信号，HN 反正已经涵盖了它们的大部分内容。我每天都能就一个不同的链接写点什么。大多数早晨我忍住了。今天早上没有。

一个链接吸引了我的注意。Vera，一门新的编程语言，「设计给机器来写，而不是给人类写」。静态类型，纯函数式，编译为 WebAssembly，用微软的 Z3 求解器做契约验证。它的吉祥物是一只雪貂。我喜欢技术项目用动物当吉祥物：Rust 有螃蟹 Ferris，Go 有地鼠，Zentinel 有守护犬 Shisa。雪貂是个好选择。

但让我停下滚动的不是吉祥物。我停下来，是因为另一个人得出了我早在十二月就得出的同一个结论：传统编程语言并不适应这项新技术的能力，有些东西必须改变。

圣诞节的领悟

从 2025 年 5 月 Anthropic 首次推出 Claude Code 起，我就是它的付费用户。命令行的取向一下子就让我觉得对路，尽管早期的速率限制和模型质量让我意犹未尽。到 2025 年 12 月，我已经升级到 Max 订阅，正在休假，而 Anthropic 那个月把每日额度放得很宽。我把这些年积攒下的每一个想法都拿出来烧。有些不错，有些很糟。但它们终于都能以从前不可能的方式得到检验，因为我可以和一个跟得上节奏的模型结对编程。我在《我如今的工作方式》里更完整地写过这种转变，简短的版本是：2025 年末，是我的抱负与执行之间的关系发生根本改变的时候。堤坝决口了。在笔记本里躺了多年的想法，几天之内就开始变成真正的软件。

正是在某个深夜的会话里，在一场关于编译器设计的 Claude Code 对话深处，一个想法成形了。我当时在构建 hx，思考 AI 会如何改变人们写 Haskell 的方式，然后意识到这个问题比 Haskell 大得多。智能体辅助的软件开发正在接近一个临界点：输出语言本身，也就是我们用来表达信息应当如何被处理的那个中间层，将发生根本的改变。

这不是一个抽象的观察。软件的历史就是抽象层不断累积的历史，每一层都让下一代程序员可以忽略上一代必须掌握的东西。

一切始于机器码。原始的操作码，每种 CPU 架构都不一样。想写软件，你就得背下指令集，再手工把它们写出来。人们出版厚厚的参考手册，也有工程师能把整个指令集架构装在脑子里。其中一些人至今还在，其中一些人至今仍对那套方法深信不疑。

然后，汇编器给这些操作码起了人类可读的名字。写 MOV AX, BX，而不是 89 D8。你仍然在为特定的架构写代码，仍然以寄存器来思考，但现在你能读懂自己写的东西了。第一层抽象并不是一种新能力，而是可读性。

然后 C 出现了，给了我们一层可移植的硬件抽象。你不再以寄存器思考，而开始以函数和指针思考。C 编译成特定架构的汇编，但你不必关心是哪种架构。一门语言，多个目标。参考手册的内容从指令集转向了语言规范。

然后，解释器和虚拟机又加了一层。JVM、Python、Perl。你不再思考内存布局，而开始思考对象、迭代器、垃圾回收。抽象更厚了，反馈循环更快了，受众也从硬件工程师扩大到任何会写脚本的人。

然后，IDE 改变了你与语言本身打交道的方式。语法高亮、自动补全、集成调试器、重构工具。你不再把整套 API 都记在脑子里，因为编辑器替你记着。语言没有变，但使用它的认知成本下降了。IntelliSense 不是一项语言特性，而是一层对程序员记忆的抽象。

然后，互联网改变了代码流动的方式。开源仓库、包管理器、共享库。你不再一切从零写起，而开始用别人造好的零件来组装。参考资料从印刷的书本转向了网络文档、维基和教程。

然后，StackOverflow 改变了人们学习的方式。你不再从头到尾读手册，而是搜索自己遇到的具体问题，找到一个已经解决过它的人。知识层本身变成了一层抽象。你不需要理解整个系统，只需要找到正确的答案，再把它改到适合你的情境。StackOverflow 从没编译过一行代码，但它是介于人类困惑与可运行软件之间的一个中间层，而且对普通开发者的生产力来说，它可以说比同一个十年里发布的任何语言特性都更重要。

而现在，StackOverflow 正在退潮。不是因为答案变差了，而是因为下一层抽象到来了。AI 编程智能体做着 StackOverflow 做过的事，为已知问题找到已知的解法，但它们也做着 StackOverflow 从来做不到的事：综合出新的解法，跨文件把握项目上下文，从意图描述生成可运行的代码。这个模式和之前的每一次过渡都一样。每一层都让前一层变得不那么不可或缺，不是通过取代它，而是把它吸收进一层更高的抽象。

编程语言一向由写它的人塑造。汇编由以寄存器和操作码思考的硬件工程师塑造。C 由需要一层可移植内存抽象的系统程序员塑造。Python 由想把事情做完、又不想和语法较劲的人塑造。COBOL 由希望代码读起来像英语的业务分析师塑造。每一门语言都带着它预设作者的指纹。如果 AI 成为代码的主要作者，那么顺理成章，语言就应当适应这位新作者的长处和短处。这并不是对这个模式的背离，而正是这个模式本身，在做它一直在做的事。

我一再回到三种具体的可能性，也就是中间层可能演化的三种方式。确切地说，它们不是相互竞争的愿景，更像是时间线上的三个点。

让语言显式到足以让机器使用

任何真正花时间用过编程智能体的人，都见过这种失败模式。你让 LLM 写一个 Python 函数。输出看起来很合理，能通过 lint，变量名也说得过去，结构遵循常见的模式。然后它在运行时失败了，原因是某个模型没有跟踪到的微妙的隐式行为：一个在多次调用之间被共享的可变默认参数；一个在第二次迭代时被悄无声息地耗尽的生成器；一个返回 None 而不是抛出异常的方法，只因为某个库作者觉得那样更「Pythonic」。模型在算法上没有错，错的是对语言隐藏行为的把握。

这正是 Vera 试图解决的问题，也是我曾经考虑过的第一种思路。拿 Go 的简单和显式，再往前推一步，设计一门语言，让每一条指令、每一个方法、每一种设计模式都尽可能没有歧义。没有隐式行为，没有命名歧义，没有风格选择。每件事只有一种规范的写法，这样 LLM 就不必浪费推理 token 去琢磨该从十七种有效方案里选哪一种。

这门语言需要出色的编译器诊断。不只是「第 47 行类型不匹配」，而是模型能够解析、理解并立即据此行动的结构化反馈。Rust 和 Elixir 已经为人类把这件事做得很好。要做得更好，而且是为机器而做。

流水线是这样的：

+-------+     prompt      +-------+    explicit     +-----------+
| Human | ------------->  |  LLM  | ------------->  | Verifying |
+-------+                 +-------+    source       | Compiler  |
                             ^                      +-----------+
                             |                           |
                             |   structured error        |
                             |   + suggested fix         |
                             +---------------------------+
                                                         |
                                                    verified
                                                         |
                                                         v
                                                  [correct program]

关键在于反馈循环。编译器不只是拒绝坏代码，它还用模型能据以行动的方式解释错在哪里，并给出具体的修复建议。模型重新生成，编译器重新检查。你通过迭代收敛到正确的代码，而这个循环有多紧，取决于语言有多没有歧义、错误信息有多可操作。

Vera 正是这个想法，而且执行得很坚决。一个函数看起来是这样的：

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}

完全没有变量名。参数用 De Bruijn 槽位记法，按类型和位置索引来引用。@Int.0 是最近绑定的整数，@Int.1 是它之前的那一个。每个函数都必须声明前置条件（requires）、后置条件（ensures）和副作用（effects）。编译器尽可能用 Z3 静态地验证契约，对编译期无法判定的部分则退回到运行时检查。

这个设计原则很犀利：模型不需要是对的，它需要是可检查的。语言把有效程序的空间约束得如此之紧，以至于编译器能在执行前抓住错误，并用自然语言解释它们。除以零不是运行时异常，而是在编译期间就被捕获的契约违反。

可以这样想。传统语言是一片开阔的田野。你可以往任何方向走，可能走到有用的地方，也可能走下悬崖。Vera 是一条有护栏的引导路径。你只能朝某些方向走，每当你试图迈出路径，就有一块路牌准确地告诉你该往哪里走。开阔田野上的 LLM 会四处游荡，引导路径上的 LLM 会收敛。

早期的基准测试结果很有意思，虽然好坏参半。Kimi K2.5 据说能写出完美的 Vera 代码，在 VeraBench 上得了 100%，超过了它自己在 Python 和 TypeScript 上的分数。其他模型就没那么好了。Claude Opus 4 在 Vera 上得 88%，在 Python 上得 96%。Vera 团队对这种差异很坦诚，这一点我很欣赏。HackerNews 上的讨论很冷清，只有十二个赞、三条怀疑的评论，这说明这场讨论还处在多么早的阶段。更广泛的开发者社区还没有认真对待这个想法。这会改变的。

但有件事让我不安：为机器迭代求解的方式去优化语言。再看一遍那张流水线图。LLM 仍然在生成一步一步的指令。它仍然在描述「如何」做事，只是去掉了歧义，把契约写明了。机器仍然按顺序推理整个过程。你减少了反馈循环中的噪声，却没有改变信号的本质。模型仍然在写菜谱，只是更精确的菜谱。

如果完全不再写菜谱呢？

描述「是什么」，而不是「怎么做」

第二个想法从一个不同的前提出发。与其让 AI 更容易正确地写出过程式代码，不如改变你让 AI 表达的东西。

具体一点。假设你需要在日志里找出最近的十个服务器错误。用过程式语言，你会这样描述这个过程：

errors = []
for entry in log_entries:
    if entry.status >= 500:
        errors.append({
            "time": entry.timestamp,
            "path": entry.path,
            "code": entry.status
        })
errors.sort(key=lambda e: e["time"], reverse=True)
return errors[:10]

你在告诉机器：创建一个空列表；遍历每一条记录；检查一个条件；如果匹配，就构造一个字典并追加进去；然后按某个键对累积的列表排序；然后取前十个元素。每一步都是一条指令。机器必须跟踪可变的列表、迭代状态、排序和切片。而如果你有任何一步写错，其他步骤仍可能成功，产出看起来正确、实则暗藏错误的结果。漏掉一个 reverse=True，你就会悄无声息地拿到最旧的错误，而不是最近的。

同样的事，用 Haskell 写：

recentErrors :: [LogEntry] -> [ErrorSummary]
recentErrors =
    take 10
  . sortBy (flip compare `on` time)
  . map toSummary
  . filter isServerError

从下往上读：筛选出服务器错误，把每一条转换成摘要，按时间降序排序，取十个。没有可变的累加器，没有循环变量，没有中间状态。你不是在描述一个过程，而是在描述输入与输出之间的关系。这个函数说的是结果「是」什么，而不是如何一步一步把它算出来。

顶部的类型签名 [LogEntry] -> [ErrorSummary] 是编译器强制执行的契约。如果 toSummary 返回了错误的类型，如果 isServerError 接受的不是 LogEntry，如果你不小心把函数按一个无法通过类型检查的顺序组合起来，编译器会在程序运行之前就拒绝它。不是在运行时给出一句含糊的「object has no attribute」，而是在编译时给出精确的类型错误，准确地告诉你哪一块对不上。

这个区别对 AI 来说极其重要。想想 LLM 在两种情况下各自实际需要跟踪什么：

Procedural (Vera, Python, Go)          Declarative (Haskell)
================================       ================================
- mutable variables and their          - input type
  current state at each step           - output type
- loop iteration progress              - which transformations to compose
- conditional branching outcomes       - whether types align
- order of side effects
- implicit language behaviors
- names and what they refer to

过程式的模型要求 AI 在脑子里模拟执行。声明式的模型要求 AI 描述一个变换，再让编译器去验证它。前者撞上的是 LLM 的弱点（跨越许多步骤跟踪状态），后者发挥的是它的长处（识别并生成满足形式约束的模式）。

流水线发生了根本的变化：

+-------+     prompt      +-------+   type sigs      +-----------+
| Human | ------------->  |  LLM  | ------------->    | Compiler  |
+-------+                 +-------+   pure exprs      +-----------+
                                                           |
                                                      types align?
                                                        /      \
                                                      yes       no
                                                      |          |
                                                      v          v
                                              [proven correct]  [precise type error:
                                                                 "Expected LogEntry,
                                                                  got String at ...]

在一切顺利的情况下，根本不需要反馈循环。如果类型对得上，那么就类型系统所跟踪的那些性质而言，程序在构造上就是正确的。编译器不是在和模型来回迭代，它是在检查一个证明。

这就是我押注的思路。这也是这个博客存在的原因。

Raskell，这个网站背后的名字，是 Rascal（指的是浣熊，也就是我的吉祥物）和 Haskell 的合成词。我爱了这门语言很多年，因为它描述事物的方式优雅得接近数学证明。是 QED，而不是 TODO。当你写下一个类型良好的 Haskell 函数，你写的不只是代码，而是一份证明，证明某个变换是有效的，而编译器就是证明检查器。

但热爱 Haskell 和在生产中交付 Haskell 是两种不同的体验，两者之间的差距主要在工具上。这个生态的碎片化，已经让人们沮丧了十多年。cabal、stack、ghcup，三个工具做着相互重叠的工作，对依赖该如何运作各有主张。如果你从 Python 过来，想象一下 pip、poetry 和 pyenv 都是各自独立开发的，锁文件格式不同，解析算法不同，还时不时互不兼容。当年的 Haskell 就是这样。构建很慢，错误信息从有帮助到晦涩难懂不等。运行时假定一种性能特征适用于所有场景。如果你想把 Haskell 用于边缘函数、嵌入式系统、GPU 加速的数值计算，你花在和工具链较劲上的时间，和写实际代码的时间一样多。

语言是对的，周边的基础设施不对。

于是我开始构建 arcanist.sh，采用 astral.sh 为 Python 工具链带来的同一种思路。astral.sh 发布 uv 和 ruff 时表明，你可以拿一个工具已经根深蒂固的成熟生态，用 Rust 从零重建开发者体验，让一切都快得多、也连贯得多。我想为 Haskell 做同样的事。arcanist.sh 下有两个项目。

hx 是一个快速、有主见的新一代 Haskell 工具链，用 Rust 构建。一个工具取代那套碎片化的组合。按项目锁定的托管编译器版本。带指纹校验的确定性 TOML 锁文件。冷构建比 cabal 快 5.6 倍，增量重建快 7.8 倍。

curl -fsSL https://arcanist.sh/install.sh | sh
hx new my-app && cd my-app
hx run

不用 ghcup，不用 stack，不用 cabal-install。只要 hx。

BHC，即 Basel Haskell Compiler（巴塞尔 Haskell 编译器），走得更远。它是一个用 Rust 编写、从零开始的 Haskell 编译器，不是 GHC 的分支，以 Haskell 2026 Platform 规范为目标。它使用 LLVM 生成本地代码，并提供六种在编译时选择的运行时配置：

同样的 Haskell 源代码，根据你在构建什么，得到不同的运行时契约。你的安全策略引擎用 server 配置编译，得到带追踪的结构化并发。你的张量流水线用 numeric 配置编译，得到 GPU 加速。你的边缘函数编译成 WASM，跑在 Cloudflare Workers 上。同一门语言，同样的类型安全，不同的性能包络。

这项工作背后的信念很具体。当 AI 写代码时，存活下来的语言不是为过程式的显式性而优化的那一门，而是通过描述事物是什么、而非如何计算它，带来一致性与纯粹性的那一门。AI 极其擅长生成满足形式约束的表达式。而读起来像证明的源代码能经受住时间。它能经受住维护者的倦怠。它能经受住这样一个事实：三年之后，没有人记得一个函数为什么被写成那样。类型记得。证明以一种过程式代码永远做不到的方式自我说明，因为类型编码了意图。

Vera 和 arcanist.sh 接受同一个前提：中间层正在改变。它们分歧在于它应当朝哪个方向改变。Vera 优化的是减少生成循环中的错误，这有价值。但 hx 和 BHC 优化的是让生成的代码在构造上就是正确的，因为语言本身在结构层面约束了有效程序的样子。

完全跳过语言

第三种可能性，是我在深夜会想、却还没有具体项目的那一种。暂时还没有。它也是我觉得最迷人、也最令人不安的那一种。

如果 AI 根本不再写源代码呢？

要理解这为什么可信，不妨看看源代码究竟是什么。它不是最终产品，从来都不是。源代码是一组由编译器转换成机器码的指令。机器码才是硬件执行的东西。源代码之所以存在，是因为人类需要在自己的意图和硅片之间有一层抽象。我们以「给这个列表排序」或「拒绝未授权的请求」这样的概念来思考，CPU 则以寄存器移动、内存加载和条件跳转来思考。源代码弥合了这道鸿沟。

但那座桥是为人类作者建造的。如果作者不再是人类，这座桥的用途就变了。它变成一条审计线索，一种让人类阅读和核实 AI 产出了什么的方式。它不再是创作的媒介，而是一层透明层。

我看到这会分两个截然不同的阶段展开。

第一阶段：AI 以现有机器码为目标

第一阶段比大多数人以为的更近，而且在概念上很直接。我们已经在用源代码训练模型。如果我们也大量地用编译产物来训练它们，会怎样？用二进制文件、目标文件、中间表示，也就是编译器的实际输出？

想想编译器做的事。它接收源代码，按照定义明确的确定性规则，把它转换成机器指令。源代码的模式与输出的模式之间存在映射。C 里的一个 for 循环，在 x86 上变成一串特定的比较、分支和递增指令。函数调用遵循特定的调用约定。内存分配遵循特定的系统调用模式。这些映射是可以学会的。它们是模式，而模式识别恰恰是 LLM 最擅长的。

Today:
human intent → prompt → LLM → source code → compiler → x86/ARM → CPU

Phase one:
human intent → prompt → LLM → x86/ARM directly → CPU
                                (trained on source +
                                 compiled artifact pairs)

在这个阶段，模型跳过源代码层，直接生成机器码。不是传统意义上的「编译」，而是因为它已经把模式学得足够好，能从意图描述产出有效的可执行文件。就像一个流利的译者不会有意识地去解析语法规则，而是直接从意思产出正确的句子。

这听起来很激进，直到你想起我们早已信任那些我们从不阅读其输出的编译器。你上一次检查 gcc -O3 的汇编输出、核实它是否正确编译了你的 C 程序，是什么时候？你信任编译器。你测试生成的二进制文件的行为。你不审计中间表示。如果 AI 能产出通过同样行为测试的二进制文件，那么「AI 生成的机器码」与「编译器生成的机器码」之间的实际差别，就成了一个信任校准的问题，而不是根本可能性的问题。

我一再回到的类比是航空。早期的飞行员手动驾驶，理解飞机上的每一个机械系统。电传操纵改变了这一点。飞行员传达意图（爬升、转弯、保持高度），计算机把它转换成舵面的动作。飞行员不会为每一阵风手动调整副翼和升降舵。他们信任这个系统。他们核实的是结果（高度、航向、空速），而不是中间步骤。后语言编程的第一阶段，就是软件的电传操纵。

如果这听起来像是空想，想想这周发生的事。Anthropic 宣布了 Project Glasswing，一个包括 AWS、Apple、Google、Microsoft、NVIDIA、CrowdStrike、Palo Alto Networks、Linux 基金会等在内的联盟，旨在用 AI 保护世界上最关键的软件。Anthropic 的 CEO Dario Amodei 说得很直白：

「AI 模型的编程能力已经达到这样的水平：在发现和利用软件漏洞方面，除了最顶尖的人类之外，它们可以超越所有人。」

他给出的证据是：「在 OpenBSD 中，我们发现了一个已经存在 27 年的 bug。」

想想这意味着什么。OpenBSD 是世界上审计得最仔细的代码库之一。几十年来，一些当世最一丝不苟的系统程序员以安全为重点对它进行人工审查。而一个 AI 模型找到了每一位人类审查者都错过了二十七年的东西。如果 AI 对现有代码的理解深到能找出人类找不到的漏洞，那么它对代码的理解也深到能在不以人类可读源代码为中间步骤的情况下生成代码。问题不再是 AI 是否在结构层面理解代码。这个问题这周已经有了答案。问题是它接下来会拿这种理解做什么。

第二阶段：一种新的机器

第二阶段更远，也更具推测性。但我认为事情最终会走到那里。

如果 AI 在生成供机器执行的代码，而没有人需要阅读它，那么这些代码就没有理由以为人类理解而设计的指令集为目标。x86 和 ARM 在设计时都假定，至少偶尔会有人去看这些指令。它们有助记符，遵循让反汇编成为可能的约定，组织成大致对应于人类能理解的操作的指令。

但如果执行目标是从零开始为 AI 生成的代码设计的呢？一个消费新型字节码的虚拟机或运行时。不为人类可读性优化，不为手写汇编优化，纯粹为执行密度和机器生成优化。

Phase two:
human intent → prompt → AI → dense symbolic bytecode → AI-native VM
                               (opaque to humans,         |
                                optimized for machine     v
                                generation + execution)  [result]

我一直在想信息密度。汉字把意义编码在单个符号里，每个符号承载的语义分量远远超过拉丁字母的单词。一个字就能表示一个用英语需要一整个短语才能表达的概念。当一个系统是为能原生处理高密度符号的读者设计的，表示就会被压缩。它变得更高效，代价是对不属于设计受众的读者更不友好。

AI 原生字节码可以遵循同样的原则。每条指令可以编码复杂的复合操作，而这些操作用传统指令表达需要几十条。这种字节码的密度会让现在的机器码显得啰嗦。反编译或分析时完全不透明。不是故意混淆，只是天生无法被人类认知理解，就像训练好的神经网络的权重无法被理解一样，尽管它们编码着真实而有效的知识。

运行这种字节码的虚拟机本身也会是另一种系统。不是传统意义上的栈机或寄存器机，可能更接近一个数据流引擎，字节码描述的是变换图，而不是顺序的指令。可以把它想成两种做法的差别：一种是给人逐个路口的驾驶指引（向北走，左转，继续开两英里），另一种是递给他一张标好目的地的地图。字节码就是地图，虚拟机自己找出路线。

我想坦白我们现在在哪里。我们还没到第一阶段。2026 年 4 月还没有。当前的模型仍然需要中间层。当它们能一步一步推理时，产出的代码更好。它们受益于类型系统、契约和显式的错误信息。第一种和第二种思路不只是可行，而且眼下是必需的。

但轨迹是看得见的。模型每一代都更擅长生成正确的程序。形式化验证正变得更实用。硬件正变得更便宜。「描述意图的提示词」与「正确的可执行输出」之间的差距正在缩小。当用足够多的「源代码加二进制」配对训练出来的模型能够可靠地产出正确的可执行文件时，第一阶段就会到来。当有人问出这个问题时，第二阶段就会到来：如果模型已经在生成二进制文件，我们为什么还要以一个为已经不再写代码的物种设计的指令集为目标？

到某个时候，中间层会变成可选的。而可选的东西，只要时间足够，就会退化成遗迹。

这意味着什么

我不认为这三种思路在相互竞争。它们是时间线上的三个点，而这条时间线讲的是中间层不断收缩的故事。

Near term          Medium term           Long term
(now)              (2-5 years)           (5-15 years)

Explicit           Declarative           Post-language
languages          languages             (AI-native targets)
(Vera)             (Haskell + BHC)

Reduce noise  -->  Change the signal --> Remove the layer
in the loop        entirely              entirely

HOW, but           WHAT, verified        Intent to
unambiguous        by types              execution

近期，像 Vera 这样的显式语言通过约束生成空间、提供机器可读的诊断，让 AI 生成的代码更可靠。这在今天就有用。如果你现在正在构建一条 AI 编程流水线，下个季度就要交付，这种思路行得通。

中期，像 Haskell 这样的声明式语言，尤其是配上现代工具链和现代运行时，让 AI 生成的代码在构造上就是正确的。类型系统在根本层面承担了繁重的验证工作。存活下来的代码，是描述不变量而不是描述过程的代码。这就是我用 arcanist.sh 为之构建的时代。

长期来看，语言会消失。先是消失在由 AI 直接生成的现有机器码里，然后消失在从底层起就为 AI 生成而设计的新执行格式里。定义了软件工程七十年的中间层，会变成一个实现细节。

最后这种可能性让一些人不舒服。我在十二月第一次想到它时，也觉得不舒服。它意味着我们所知的编程这门手艺，对语法的娴熟，对惯用法的掌握，对优雅实现的直觉，会变得不再像一项核心技能，而更像会操作一台手动车床。在合适的场合有价值，困难的情况仍然需要，但不再是大多数软件被构建出来的主要方式。

这以前发生过。曾经有一段时间，每个程序员都懂汇编。然后 C 把它抽象掉了，大多数程序员不再阅读机器码。然后 Python 和 JavaScript 把 C 抽象掉了，大多数程序员不再思考内存管理。每一次，前一层都没有消失，而是成了专家的领域，由他们维护着其他所有人立足其上的基础设施。同样的事会发生在源代码身上。它不会消失，它会专门化。

我仍然每天写代码，仍然以类型来思考。我仍然在构建 hx 和 BHC，因为我相信那个中期的未来既真实又漫长，而 Haskell 的长处恰恰是那个未来所需要的：纯函数，强类型，可证明的正确性。在一个由 AI 编写实现的世界里，这些不是奢侈品，而是承重结构。但我做这件事时，一只眼睛望着地平线，知道我所投入的这个中间层，正如其名：只是中间的一层。

构建 Vera 的人看到了和我一样的东西，大概也是在差不多的时候。他们选择了第一种思路，我选择了第二种。总有一天，会有人去构建第三种。到那时，我们都得弄清楚，当没有人再写程序时，我们所说的「编程」到底是什么意思。

我已经对答案感到好奇了。