重申一遍，我并不是为了否认尖端的 PLT 研究，如果没有这些研究者经年累月的工作，可能我不会作出 Chiba。

Let me reiterate: I am not here to deny the value of cutting-edge PLT research. Without the years of work by these researchers, I probably couldn’t have built Chiba.

当我重新翻开皮埃尔·布迪厄的《区隔》时，我看到的不再是 20 世纪 60 年代法国中产阶级对咖啡、画展和古典乐的精致趣味，而是当代技术社区中那道日益深重的、不可逾越的鸿沟。

When I reopened Pierre Bourdieu’s Distinction, what I saw was no longer the refined tastes of 1960s French bourgeoisie for coffee, gallery openings, and classical music, but rather the deepening, insurmountable chasm within today’s technology community.

布迪厄告诉我们：“品味”从来不是自然的，它是阶级的自我标识。一种文化形式之所以被赋予”高贵”的地位，往往不是因为它在功能上更优越，而是因为它建立了某种”难以抵达的复杂性”，从而完成对大众的智力放逐。这种逻辑在艺术界表现为对抽象符号的迷恋，而在编程世界里，则表现为对 PLT 黑话的疯狂堆砌。

Bourdieu tells us: “taste” is never natural — it is a class marker. A cultural form is granted “noble” status not because it is functionally superior, but because it erects a wall of “inaccessible complexity,” thereby completing the intellectual exile of the masses. In the art world, this manifests as an obsession with abstract symbols. In the programming world, it manifests as the frantic accumulation of PLT jargon.

于是，我开始审视那些被奉为神谕的函数式原语，以及那些以此为生的学术贵族。我意识到，所谓的”高阶抽象”与”纯粹性”，本质上不过是数字时代的文化资本垄断。他们通过垄断”编译器教育”这一拉丁语式的秘技，在冰冷的机器与劳动的程序员之间，硬生生地塞进了一套洛可可式的装饰美学。

So I began to scrutinize those functional primitives held up as divine revelation, and the academic aristocrats who live off them. I realized that so-called “higher-order abstraction” and “purity” are, at their core, nothing more than cultural capital monopolization in the digital age. By monopolizing “compiler education” — that Latin-like secret art — they have forcibly inserted a Rococo decorative aesthetic between the cold machine and the laboring programmer.

在这场名为”高级”的审美骗局中，Monad 变成了它的勋章，而范畴论则成了它的礼仪。正如布迪厄解构资产阶级的审美一样，我们也必须解构这种学术傲慢。因为在清水混凝土般的机器事实面前，一切不能转化为机器指令的虚假优越，都终将在一场野兽派的审美风暴中崩塌。

In this aesthetic con game called “advanced,” Monad has become its medal of honor, and category theory its etiquette. Just as Bourdieu deconstructed bourgeois aesthetics, we too must deconstruct this academic arrogance. Because in the face of the bare-concrete reality of the machine, all false superiority that cannot be translated into machine instructions will ultimately crumble in a Brutalist aesthetic storm.

审美差异：代码作为身份的纹章

Aesthetic Differences: Code as Heraldic Crest

代码从来不只是逻辑，它是程序员的阶级品味。

Code has never been just logic — it is the class taste of the programmer.

你打开一个 C 程序员的代码仓库，看到的是严丝合缝的结构体对齐、手动管理的内存池、每一行都带着一种古板的对称感——就像一座哥特教堂的飞扶壁，每根柱子都有结构上的理由。古典主义者追求的是”每一块石头都在承重”。你可以不喜欢它的笨拙，但你不能否认它的诚实。

You open a C programmer’s repo and see meticulously aligned structs, hand-managed memory pools, every line carrying a stubborn symmetry — like the flying buttresses of a Gothic cathedral, every column with a structural reason for being. The classicist pursues “every stone bears weight.” You may not like its clumsiness, but you cannot deny its honesty.

然后你打开一个 Java 项目。二十层目录结构，八个抽象接口后面藏着一个 if-else。Go 更直接一些，直接告诉你：我们不需要泛型（后来又加了），我们不需要异常处理（后来又不加了）。暴发户的品味是功能性的平庸——不求优雅，但求能用；不怕重复，只怕出格。这是一种刻意的朴素，底下藏着的是对复杂性的恐惧。

Then you open a Java project. Twenty layers of directories, eight abstract interfaces hiding a single if-else. Go is more direct — it just tells you: we don’t need generics (then added them), we don’t need exceptions (and still haven’t). The nouveau riche taste is functional mediocrity — not seeking elegance, just utility; not fearing repetition, only deviation. It’s a deliberate plainness, concealing a fear of complexity underneath.

最后你打开一个 Haskell 项目。类型签名比函数体还长。一个处理 JSON 的函数，经过三层 Monad Transformer 的包裹，最终的效果和 Python 里十行代码做的事情一模一样——但是，它是”可证明正确”的。学术贵族沉溺于一种极其昂贵的、脱离世俗劳作的形式美学。代码的简洁不再是为了运行效率，而是为了体现出一种”我不需要为底层性能而焦虑”的从容。

Finally you open a Haskell project. Type signatures longer than function bodies. A JSON-handling function wrapped in three layers of Monad Transformers, ultimately doing the exact same thing as ten lines of Python — but it’s “provably correct.” The academic aristocracy indulges in an extraordinarily expensive formal aesthetic, detached from worldly labor. Code brevity is no longer about runtime efficiency; it’s about projecting an air of “I don’t need to worry about low-level performance.”

这三种审美之间的分野，不是技术路线的分歧，是阶级品味的分野。古典主义者的代码闻起来是铁锈和焊锡的味道，暴发户的代码闻起来是新装修办公室的甲醛味，而学术贵族的代码闻起来是羊皮纸和橡木书架。

The divide among these three aesthetics is not a divergence in technical approach — it is a divergence in class taste. The classicist’s code smells of rust and solder. The nouveau riche’s code smells of formaldehyde in a freshly renovated office. The academic aristocrat’s code smells of parchment and oak bookshelves.

问题在于：机器不在乎你的品味。CPU 不知道你的类型签名有多优雅。寄存器不关心你用了几层 Functor。当你的程序最终被翻译成一串 mov 和 jmp 的时候，所有的阶级标识都被剥得一干二净。在那个层面上，每一段代码都是赤裸的。

The problem is: the machine doesn’t care about your taste. The CPU doesn’t know how elegant your type signatures are. The registers don’t care how many layers of Functor you used. When your program is finally translated into a stream of mov and jmp, all class markers are stripped bare. At that level, every piece of code is naked.

伪贵族的攀附：当工业界开始”附庸风雅”

Faux Aristocracy: When Industry Starts Playing Connoisseur

大公司的语言正处于一场尴尬的**“文化洗白”**中。

The languages of big corporations are in the midst of an awkward “cultural laundering.”

TypeScript 疯狂引入越来越复杂的类型体操——条件类型、映射类型、模板字面量类型——搞到最后，类型系统本身变成了一门图灵完备的语言，程序员开始在类型层面”编程”，而真正要运行的那层逻辑反而成了附属品。Rust 执着地实现 GAT，花了六年时间争论语法，社区里每隔几个月就爆发一次关于”要不要加高阶类型”的神学辩论。

TypeScript has been frantically introducing ever more complex type gymnastics — conditional types, mapped types, template literal types — until the type system itself became a Turing-complete language, programmers started “programming” at the type level, and the actual runtime logic became an afterthought. Rust obsessively implemented GATs, spent six years debating syntax, with the community erupting every few months into theological disputes about “whether to add higher-kinded types.”

这本质上是中产阶级对贵族生活的拙劣模仿。

This is, at its core, the middle class’s clumsy imitation of aristocratic life.

就像一个富商在客厅里摆满了自己并不真正理解的抽象画，让子女学钢琴不是因为热爱音乐，而是因为”上流社会的孩子都学”。引入这些特性的根本动力，不是为了代码更好写、程序跑得更快，而是为了向外界宣布：“嘿，你看，我们也拥有某种’高级’的抽象品味。”

Just like a tycoon filling his living room with abstract paintings he doesn’t truly understand, having his children learn piano not out of love for music but because “upper-class children all do.” The fundamental motivation for introducing these features isn’t to make code easier to write or programs faster to run — it’s to announce to the world: “Hey, look, we too possess a certain ‘sophisticated’ taste for abstraction.”

但布迪厄早就说过，品味的模仿永远是拙劣的。贵族的优雅是浸泡出来的，不是买来的。你把 Haskell 的 GAT 搬到 Rust 里，它并不会自动变得优雅——它只会变成一个更复杂的借用检查器错误信息。你把依赖类型的皮毛搬到 TypeScript 里，它并不会让你的前端代码更可靠——它只会让 tsconfig.json 多出二十行没人看得懂的选项。

But Bourdieu said it long ago: imitation of taste is always clumsy. Aristocratic elegance is steeped, not purchased. Transplant Haskell’s GATs into Rust and it won’t magically become elegant — it’ll just become a more complex borrow checker error message. Transplant a veneer of dependent types into TypeScript and it won’t make your frontend code more reliable — it’ll just add twenty incomprehensible lines to tsconfig.json.

真正的问题不在于这些特性本身好不好。问题在于，引入它们的动机是社会性的，而不是工程性的。这是品味的焦虑，不是需求的焦虑。

The real problem isn’t whether these features are good or bad in themselves. The problem is that the motivation for introducing them is social, not engineering. This is taste anxiety, not requirements anxiety.

辞令的泛滥：术语的社交礼仪

如今的开发者社区变成了一场虚伪的舞会。

Today’s developer community has become a hypocritical masquerade ball.

Monad、Covariance、Algebraic Effect、Profunctor、Yoneda Lemma——这些词汇在技术论坛和推特上满天飞。一个程序员发了一条推文，描述了他如何用 Free Monad 重构了一个 CRUD 应用。底下三十条回复，没有一条问”重构之后快了多少”，全部在讨论这个 Free Monad 的实现是不是”sufficiently polymorphic”。

Monad, Covariance, Algebraic Effect, Profunctor, Yoneda Lemma — these terms fly across tech forums and Twitter. A programmer tweets about how he refactored a CRUD app using Free Monads. Thirty replies below, not a single one asks “how much faster is it after refactoring?” — they’re all debating whether the Free Monad implementation is “sufficiently polymorphic.”

这不再是技术探讨，这是一种社交礼仪。

This is no longer technical discussion. This is social etiquette.

布迪厄观察到，法国上流社会在沙龙里讨论绘画时，核心目的不是理解艺术，而是通过使用正确的术语来确认彼此的阶级身份。PLT 社区的讨论区完成了同样的功能。如果你不能在交谈中随口吐出几个范畴论术语，你就会被视为”未受过洗礼”的粗人——不配参加我们的编程语言讨论，你先写好你的业务再说吧。

Bourdieu observed that when French high society discussed paintings in salons, the core purpose was not to understand art, but to confirm each other’s class identity through the use of correct terminology. The PLT community’s forums serve the exact same function. If you can’t casually drop a few category theory terms into conversation, you’ll be regarded as an “unbaptized” boor — unworthy of participating in our programming language discussions; go finish your business logic first.

但你仔细看看那些对话的内容，真正有信息量的部分少得可怜。大量的讨论本质上是在反复确认一个已知结论：Monad 是好的，副作用是坏的，如果你不同意，那是因为你不懂。这种循环论证被包裹在精致的术语里，让局外人以为这是某种深奥的智识活动。实际上它和宫廷侍从讨论假发的卷曲方向没有本质区别。

But look closely at those conversations and the actual informational content is pitifully thin. The bulk of discussion amounts to repeatedly confirming a known conclusion: Monads are good, side effects are bad, and if you disagree, it’s because you don’t understand. This circular reasoning is wrapped in exquisite terminology, making outsiders think it’s some profound intellectual activity. In reality, it’s no different from courtiers debating the curl direction of their wigs.

这种术语的通货膨胀，掩盖的是思想本身的通货紧缩。当一个社区需要越来越多的术语来表达越来越少的想法时，它就已经从学术走向了神学。

This terminological inflation masks an intellectual deflation. When a community needs ever more terms to express ever fewer ideas, it has already crossed from scholarship into theology.

知识的阶级门槛

The Class Threshold of Knowledge

为什么大多数程序员觉得函数式编程难？

Why do most programmers find functional programming hard?

标准答案是：因为它需要数学基础，因为它的抽象层次更高，因为它要求不同的思维方式。这是学术贵族们乐于给出的答案，因为它暗示了一种智力上的等级——“你觉得难，是因为你还不够聪明。”

The standard answer: because it requires mathematical foundations, because the level of abstraction is higher, because it demands a different way of thinking. This is the answer the academic aristocrats love to give, because it implies an intellectual hierarchy — “You find it hard because you’re not smart enough.”

但真正的答案是：因为精英阶层有意识地维持了**“编译器知识的非对称”**。

But the real answer is: because the elite class has consciously maintained an “asymmetry of compiler knowledge.”

作为英国留子，我清楚地知道，如果我想从事 PLT 研究，我需要拜入格拉斯哥大学、爱丁堡大学、剑桥大学的门下。这不是因为别的地方没有聪明人，而是因为知识的生产和认证被锁死在了几个节点上。你在别处做出了一样好的工作？没用，你出师无名。没有那几所学校的背书，你的论文不会被正确的人读到，你的编译器不会被正确的人引用。

As someone who studied in the UK, I know full well: if I wanted to pursue PLT research, I’d need to apprentice myself at Glasgow, Edinburgh, or Cambridge. Not because there aren’t smart people elsewhere, but because the production and certification of knowledge has been locked to a handful of nodes. You produced equally good work somewhere else? Doesn’t matter — you lack credentials. Without those schools’ endorsement, your papers won’t be read by the right people, your compiler won’t be cited by the right people.

而这些知识圣殿做的事情，是把原本直白的、关于指令如何在硅片上流转的教育过程，替换成了某种关于”逻辑真理”的修行。他们不教你机器是怎么跑的，教你 lambda 演算是怎么推的。不教你如何造轮子，只教你如何跪拜轮子的完美形式。编译器课程从第一节就开始讲类型论，到最后一节还没碰过一条机器指令。学生毕业时能写出漂亮的类型推导证明，却不知道一个函数调用在栈上长什么样。

And what these temples of knowledge do is replace the straightforward educational process — how instructions flow across silicon — with a kind of monastic practice around “logical truth.” They don’t teach you how the machine runs; they teach you how lambda calculus reduces. They don’t teach you how to build the wheel; they only teach you how to genuflect before the wheel’s perfect form. Compiler courses start with type theory in lecture one and still haven’t touched a single machine instruction by the final lecture. Students graduate able to write beautiful type derivation proofs but unable to tell you what a function call looks like on the stack.

这种教育上的缺失，构成了程序员阶级之间最深的壕沟。

This educational deficit constitutes the deepest moat between programmer classes.

就如同 Homebrew 的作者面试 Google 没写出二叉树翻转一样——我们经年累月做出来的、千万人每天在用的程序，居然比不过 HR 的一道十行面试题重要？这不是能力的问题，这是评价体系本身被阶级品味劫持了。什么算”真正的计算机科学”，什么算”只是工程”，这条线不是按照对世界的实际贡献画的，是按照谁坐在格拉斯哥的办公室里画的。

Just like the creator of Homebrew failing to invert a binary tree in a Google interview — programs we’ve built over years, used daily by tens of millions, somehow matter less than a ten-line interview question from HR? This isn’t a competence problem. This is the evaluation system itself being hijacked by class taste. The line between “real computer science” and “mere engineering” isn’t drawn by actual contribution to the world — it’s drawn by whoever sits in an office in Glasgow.

难道 Monad 不是一种抽象工厂类？

Isn’t Monad Just an Abstract Factory?

这一节会让很多人不舒服。但我还是要说。

This section will make a lot of people uncomfortable. But I’m going to say it anyway.

所谓的 Free Monad，不过是一套昂贵的解释器模式。你定义一棵语法树，挂一个解释函数上去，然后告诉所有人这叫”将副作用从描述中分离”。Java 程序员二十年前就在干这件事了，他们叫它”命令模式”加”策略模式”。唯一的区别是 Java 程序员用的是 interface，而 Haskell 程序员用的是 data 和 class——一个穿西装，一个穿长衫，干的是同一件事。

The so-called Free Monad is nothing more than an expensive interpreter pattern. You define an AST, hang an interpretation function on it, then tell everyone it’s called “separating effects from description.” Java programmers were doing this twenty years ago — they called it “Command pattern” plus “Strategy pattern.” The only difference is Java programmers use interface while Haskell programmers use data and class — one wears a suit, the other wears a scholar’s robe, doing the same job.

而那个被吹上天的 Monad，本质上就是函数式编程圈里的**“抽象工厂类”**。它唯一的核心职能就是”延迟计算并进行上下文包装”。return 把值装进去，>>= 把值取出来处理完再装回去。当你撕掉那层”自函子范畴上的幺半群”这种玄学糖衣，你会发现它和 Java 里那些层层嵌套的工厂-代理-适配器链条一样，都是为了解决同一个问题：无法直面物理机器时产生的逻辑冗余。

And that much-hyped Monad is essentially the FP world’s “Abstract Factory.” Its sole core function is “delaying computation and wrapping context.” return puts a value in, >>= takes it out, processes it, and puts it back. When you strip away the mystical sugar coating of “a monoid in the category of endofunctors,” you’ll find it’s the same as those nested Factory-Proxy-Adapter chains in Java — both exist to solve the same problem: the logical redundancy produced by the inability to face the physical machine directly.

函数式编程的人鄙视 Java 像老太婆的裹脚布——又臭又长。但我想问一句：这些人难道没有用过网上银行吗？那些跑在 JVM 上的裹脚布代码，每天在处理几十亿美元的交易，从未因为”类型签名不够优雅”而丢过一分钱。反过来，我见过不少用 Haskell 写的项目，类型签名漂亮得可以裱起来，但性能差到连基本的并发负载都扛不住。

FP people despise Java for being like an old woman’s foot-binding cloth — long, smelly, and unwieldy. But let me ask: have these people never used online banking? That foot-binding code running on the JVM processes billions of dollars in transactions daily, never losing a cent because “the type signatures weren’t elegant enough.” Conversely, I’ve seen plenty of Haskell projects with type signatures pretty enough to frame, yet performance so poor they can’t handle basic concurrent load.

漂亮的裹尸布和难看的工作服，你选哪个？机器不在乎布料的花纹。

A beautiful shroud or an ugly set of work clothes — which do you choose? The machine doesn’t care about the fabric’s pattern.

符号主义对贵族的宣战

Symbolism’s Declaration of War on the Aristocracy

十九世纪中叶，当欧洲贵族还在沙龙里争论蕾丝褶边的层数和壁画的透视技法时，一个新玩意出现了：照相机。

In the mid-nineteenth century, while European aristocrats were still debating the number of lace ruffles and fresco perspective techniques in their salons, a new contraption appeared: the camera.

这台机器用化学和光学完成了贵族画师要学十年才能做到的事情——精确地复制现实。它没有品味，没有风格，没有学院背景。它只是忠实地记录光线打在物体上的样子。但就是这个没有品味的机器，引发了一场审美地震。当”精确再现”变成了机器就能做的事，艺术家被迫去思考一个根本性的问题：除了再现之外，艺术还剩下什么？

This machine accomplished with chemistry and optics what aristocratic painters needed a decade of training to do — faithfully reproduce reality. It had no taste, no style, no academic pedigree. It simply recorded how light fell on objects. Yet this tasteless machine triggered an aesthetic earthquake. When “faithful reproduction” became something a machine could do, artists were forced to confront a fundamental question: what is left of art besides reproduction?

结果是现代艺术的爆发。印象派、野兽派、抽象表现主义、极简主义——一场接一场的运动，核心都是一样的：撕掉装饰，暴露结构。

The result was the explosion of modern art. Impressionism, Fauvism, Abstract Expressionism, Minimalism — movement after movement, all sharing the same core: tear off the decoration, expose the structure.

马蒂斯用三笔画完一张人脸，不是因为他不会画细节，而是因为他认为那些细节是谎言。勒·柯布西耶用清水混凝土建造住宅，不是因为他买不起大理石，而是因为他认为结构本身就是美。蒙德里安把画面压缩到只剩水平线、垂直线和三原色，不是因为他的调色板坏了，而是因为他在追问：承载意义的最小结构是什么？

Matisse painted a face in three strokes not because he couldn’t paint detail, but because he believed detail was a lie. Le Corbusier built houses in raw concrete not because he couldn’t afford marble, but because he believed structure itself was beauty. Mondrian compressed paintings to nothing but horizontal lines, vertical lines, and three primary colors not because his palette was broken, but because he was asking: what is the minimal structure that carries meaning?

照相机之于绘画，就像 AI 代码生成之于编程。

The camera is to painting what AI code generation is to programming.

当 AI 可以用三秒钟吐出一个 Monad Transformer 的标准实现，当它可以毫不费力地写出你需要查三篇论文才能理解的类型签名——那些用知识壁垒筑起来的阶级护城河，就在一夜之间被抽干了。“你知道什么是 Profunctor 吗？“这个问题不再是身份验证的口令，因为任何人都可以让 AI 在五秒钟内解释得比你更清楚。

When AI can spit out a standard Monad Transformer implementation in three seconds, when it can effortlessly produce type signatures that would take you three papers to understand — those class moats built on knowledge barriers are drained overnight. “Do you know what a Profunctor is?” is no longer an identity-verification passphrase, because anyone can have AI explain it more clearly than you in five seconds.

Chiba 就是这场运动的编程语言版本。我们用限定续延取代那些精巧的 Monad 加类型体操的堆叠，就像用清水混凝土取代雕梁画栋。Continuation 是什么？它就是”把接下来要做的事情打个包”。它不需要范畴论来定义，不需要类型类来包装，它在机器层面就是一次栈的切割和一次跳转。这种野蛮的直接感，让那些习惯了在恒温恒湿的象牙塔里推演类型规则的人，感到了一种近乎肉体上的威胁。

Chiba is the programming language version of this movement. We replace the elaborate Monad-plus-type-gymnastics stack with delimited continuations, the way raw concrete replaces ornate carved beams. What is a continuation? It’s “packaging up what comes next.” It doesn’t need category theory to define it, doesn’t need type classes to wrap it. At the machine level, it’s one stack slice and one jump. This savage directness makes those accustomed to deriving type rules in the climate-controlled ivory tower feel something close to a physical threat.

我在这里说一件事：Chiba 的自举过程中，AI 生成代码的介入率极高，几乎没有人工逐行编写。我又不是没有写过 Haskell——但 Haskell 代码的 AI 辅助生成率反而比 Chiba 低得多。为什么？因为那些精巧的类型体操把 AI 也搞糊涂了。当你的语言复杂到连机器都难以生成正确代码的时候，你真的应该停下来想一想：这种复杂性到底在服务谁？

Let me state something here: during Chiba’s bootstrapping process, the rate of AI-generated code was extremely high — almost no line-by-line human writing. It’s not like I’ve never written Haskell — but the AI-assisted generation rate for Haskell code is actually far lower than for Chiba. Why? Because those elaborate type gymnastics confuse AI too. When your language is so complex that even machines struggle to generate correct code, you really should stop and ask: who exactly is this complexity serving?

Chiba：重塑”骨骼”的审美

Chiba: Reshaping the Aesthetics of the Skeleton

Chiba 想要重塑的是一种**“解剖学式”的审美**。

What Chiba wants to reshape is an “anatomical” aesthetic.

美不应该在装饰层，而应该在支撑层。不在贴面的大理石纹路里，在承重墙的钢筋排列里。不在类型签名的优雅弧线里，在栈帧布局的精确对齐里。

Beauty should not reside in the decorative layer, but in the structural layer. Not in the marble veneer’s grain, but in the rebar alignment of load-bearing walls. Not in the elegant arc of a type signature, but in the precise alignment of stack frame layouts.

一个能够直接触碰寄存器的语言，一个能够精准控制栈帧的编译器，一个从源代码到系统调用全链路透明的工具链——它的结构本身就是最高级的艺术品。这种审美是冷峻的、赤裸的、充满金属质感的。它不取悦人。它不假装自己比机器更文明。它只是如实地暴露计算的骨骼，然后让你自己决定：这根骨头该长在哪。

A language that can directly touch registers. A compiler that can precisely control stack frames. A toolchain transparent from source code all the way to syscall. Its structure itself is the highest form of art. This aesthetic is austere, naked, metallic. It doesn’t try to please. It doesn’t pretend to be more civilized than the machine. It simply exposes the skeleton of computation as it is, and lets you decide: where this bone should go.

安藤忠雄的清水混凝土建筑没有一寸多余的装饰。你走进光之教堂，看到的只有混凝土墙面上那道十字形的缝隙，阳光从外面透进来。没有彩色玻璃，没有雕塑，没有壁画。但那道光比任何装饰都更有力量。

Tadao Ando’s exposed-concrete buildings have not an inch of superfluous decoration. You walk into the Church of the Light and see nothing but a cross-shaped slit in the concrete wall, sunlight streaming in from outside. No stained glass, no sculptures, no murals. But that light is more powerful than any ornament.

Chiba 追求的就是这种东西。限定续延就是那道缝隙——它是控制流中最小的、最直接的切口，但它让一切复杂的控制模式都可以从这道口子里透进来。行多态就是那面混凝土墙——它的表面是粗粝的、裸露的，但它精确地承载了每一个字段的重量。内联汇编就是钢筋——你平时看不到它，但在需要的时候，你可以直接触摸到它，确认它在那里，确认它是你放的。

This is what Chiba pursues. Delimited continuations are that slit — the smallest, most direct incision in control flow, yet allowing all complex control patterns to stream through. Row polymorphism is that concrete wall — its surface rough and exposed, yet precisely bearing the weight of every field. Inline assembly is the rebar — you don’t see it normally, but when needed, you can reach in and touch it directly, confirm it’s there, confirm you placed it.

当整个函数式编程世界都在往洛可可的方向走——更多的类型层、更多的抽象层、更多的装饰层——Chiba 选择往相反的方向走。剥掉一切，直到只剩下骨骼。然后看看这副骨骼能不能自己站起来。

While the entire FP world marches toward Rococo — more type layers, more abstraction layers, more decorative layers — Chiba chooses to walk in the opposite direction. Strip everything away until only the skeleton remains. Then see if that skeleton can stand on its own.

终章：致 Agda 们——那个昂贵的花瓶

Finale: To the Agdas of the World — That Expensive Vase

如果一个程序不能在 20ms 内响应，不能像 C 一般顺滑地运行，那么它即使在逻辑上再怎么”可证明正确”，也不过是一个华丽的花瓶。

If a program can’t respond within 20ms, can’t run as smoothly as C, then no matter how “provably correct” it is in logic, it’s nothing more than an ornate vase.

AWS 的 IAM 策略引擎使用 Lean4 完成了形式化证明。证明做完之后，他们马上开始了用 C++ 的重写工作。

AWS’s IAM policy engine was formally verified using Lean4. Once the proof was complete, they immediately began rewriting it in C++.

这件事值得反复咀嚼。世界上资源最丰富的云计算公司，用了最先进的定理证明器，验证了最关键的安全策略——然后转头用 C++ 重写了整个东西。为什么？因为 Lean4 的性能扛不住生产负载。逻辑上无懈可击的代码，在物理上站不住脚。

This deserves chewing over. The world’s most resource-rich cloud computing company used the most advanced theorem prover to verify its most critical security policies — then turned around and rewrote the whole thing in C++. Why? Because Lean4’s performance couldn’t handle production load. Code that was logically impeccable couldn’t stand on its feet physically.

正如 Agda 们那些精致到令人窒息的类型推导——每一条证明都完美无缺，每一个项都有其范畴论解释，在象牙塔的陈列柜里熠熠生辉。但它们在现实世界的泥淖里踏不出一步。你不能用 Agda 写一个数据库。你不能用 Coq 写一个文件系统。你甚至不能用 Idris 应付一个稍微复杂一点的 Web 请求，因为第一个 IO 操作就会让你的编译时间膨胀到无法忍受。

Just like Agda’s suffocatingly exquisite type derivations — every proof flawless, every term with its category-theoretic interpretation, gleaming in the ivory tower’s display case. But they can’t take a single step in the mud of the real world. You can’t write a database in Agda. You can’t write a filesystem in Coq. You can’t even handle a moderately complex web request in Idris, because the first IO operation will inflate your compile time to something unbearable.

这些语言是花瓶。精美的、昂贵的、值得欣赏的花瓶。但花瓶的命运就是待在壁炉架上。你不会用它来盛水喝，更不会拿它去耕地。

These languages are vases. Exquisite, expensive, worth admiring vases. But a vase’s destiny is to sit on the mantelpiece. You won’t drink water from it, much less plow a field with it.

Chiba 不想做花瓶。Chiba 想做的是那种粗砺的陶碗——拿在手里有重量，放在桌上能盛饭，摔在地上碎了就碎了，再烧一个就是。它不追求完美的釉面，不追求无懈可击的形式化证明，只追求一件事：能用。

Chiba doesn’t want to be a vase. Chiba wants to be that rough clay bowl — heavy in the hand, able to hold rice on the table, and if it breaks on the floor, so be it, fire another one. It doesn’t pursue a perfect glaze, doesn’t pursue an airtight formal proof, only pursues one thing: it works.

代码是用来运行的，不是用来供奉的。

Code is meant to run, not to be enshrined.