渐进类型与归责——软硬缝隙处也有一条定理
这是软化逻辑的又一个实例，这次软化的是"类型系统"，而它带来了一条我们一直缺失的定理。当你不再问"是有类型还是无类型"，转而问"这个边界的置信度有多高"，编程语言理论中的一个经典结果就会豁然清晰。
软化：渐进类型——Siek–Taha（2006）
那个棘手的问题是：有类型代码和无类型代码能否共存于同一个程序？经典答案是不能——要么整个程序都经过静态检查（安全但僵硬），要么整个程序都是动态的（灵活但脆弱）。渐进类型（gradual typing）的洞见在于拒绝这个二分法。取而代之：让两者共存于同一个程序中，每一次跨越边界都触发一次运行时转换（cast），在值经过时对其进行检查。
有类型的一侧做出保证；无类型的一侧不做任何保证。在缝隙处，一次运行时检查（转换）要么确认值符合类型，要么拒绝它。不是"有类型或无类型"的硬分割，而是一个带有受检缝隙的光谱（软过渡）。转换是唯一新增的机制——其余一切照旧。
映射——harness 本身就是一个渐进类型化的程序
产物一开始是无类型的——LLM 自由生成的文本、代码，任何冒出来的东西。它们逐步硬化：你为某个子树写一个 spec，一个测试 harness 运行起来，一道机械式的关卡检查结果。每一次软→硬的跨越都是一次转换，而一次转换就是一道关卡（gate-theory）。人与 harness 协商的可写/默会缝隙，正是那条有类型/无类型的边界：人的一侧写自由文本，机械的一侧在它流向下游之前，拿一个 spec 去检查它。
这不是比喻——范畴结构是完全相同的。渐进类型系统是源代码的 harness；harness 是 AI 产物的渐进类型系统。
我们由此得到的定理：归责——Wadler–Findler 的责任演算（blame calculus）
当一次转换失败时，该由谁负责？一条经典定理说："类型良好的程序不可能被归责。" 当一次运行时检查在某个边界上失败，责任是被机械地分配的——不靠启发式，不靠某个裁判，而是沿着来源（provenance）回溯：该边界无类型的那一侧被记上一笔。你沿着失败的转换向后追溯责任，直到抵达最后一道通过了的机械关卡（如果没有关卡通过过，就追溯到自由文本的源头）。那个位置就是真凶。
对应到 harness 上： 藏在机械关卡后面的子树不可能是真凶。当下游出了问题，责任沿着来源边向后流动，直到那个置信度最低的跨越点。真凶认定不再是一种启发式，而变成一种演算。这把modal-status-labels的置信度这一维，磨成了一种责任排序：我们知道的不只是某个子树不可靠，还知道该先归责给上游的哪一次跨越。
诚实的告诫：语义关卡的转换并不完美
责任定理假设转换是完美的——一个值要么通过要么失败，没有模糊地带。现实是：语义关卡是不透明的。一道容差为 α 的关卡可能放过一个坏值（概率 ≤ α），于是责任的指向就会比实际的边界多走一步，落到下游。所以责任的结论也继承了这份置信度账本："不可能被归责，其置信度为关卡的 1−α。" 从真凶到失败点，这条链上的每一道关卡，都会从你的置信度中扣除它的误差。
这不是缺陷——这正是operationalizing-tolerances的意思。责任判定的锐利程度，取决于你的关卡有多锐利。
一句话
软硬缝隙不只是检查所在之处——它也是责任的判定之处，躲在一道机械关卡后面，你就被证明是清白的（直到这道关卡测得的 α 为止）。