1. 关系式编程的“无尽多态”

在Prolog里，(x+1=2) 不需要x的值，因为x本身就是(+)函数可以infer出的变量（就像解构）
甚至，自然数 (x+y=2) 也不需要，这是因为变量不被视为“右值” “左值”，而更像“等位值”或者“应后值(x=inHole 1)”

为了将DFS的推理过程与递归结合，一般是用Peano“链表数”简化自然数相加的意思： `append_out(x, [1],[1,1])`
如果把(+)视为assert，x,y 视为类型变量，甚至是程序……或者反之？我们就有了“兼容一切可能性”的检查器。这也是SAT算法的应用。

因为，这时“栏目答(lambda)”新建的变量，不是“要被赋值的盒子”，而是“约束的孔洞”。
“变量的容器”对函数就不再是黑箱，而是“提问的基础”。

2. 可以在函数执行前assert的“类型标注”

有句话叫“没有类型比def本身的实现，更能表达它的类型。”
无论def,class还是更复杂的结构，typehint的本质是被独立执行的assert语义，它是一个“子语言”。
写一个typer，其实就是写一个解释器，然后，让它停机。
这样就肯定不能体现“流控语意”，比如 for,if,throw，因此它也会引入模糊性，也就是 soundness vs completeness （误报时的过严和“执行时”过慢）

比如 union type “有联类型”就能比C的类型更好对应 (isXX? A():B()) 这种语法，因此更sound： 优雅的程序会“镜像”它所处理数据的结构，类型亦然。
到这里，我们已经看到“类型和程序同构性”里的三态：事后检查(TS)、同步构造(程序就像x,y)、事前求解(Prolog)

3. 程序的等价性

既然我们知道了关系式编程类似SAT，它的基石是 unify(A,B) 的成立、组合或分支，程序显然也有着相等性

(x=>x) 等价 (y=>y) 是栏目答演算里的一个“定理”，它的成立前提在TypeScript也可以表达： 如果类型签名不同，函数不可能相等。

但“等价”似乎是另一种： `f(A,B) 等价 ((A,B,_x)=>f(B,A))(B,A,0)` 并不比上面的“定理”困难，而且它的“类型签名”相差很大

“类型即命题，程序即证明” 在此到底是指什么呢？请结合要点1“等位值”探讨。

上面的等价性，在TypeScript上依赖于 <A,B> 变量被「抽象」成为不同类型，但是当涉及“字面类型”时：
`chkstk=(n)=>(n==0)? 0 : chkstk(n-1)+1`
如何证明若有 nat(n) ，chkstk会停机？ 请结合要点1讲解

https://chat.librechat.ai/share/_DzXZONw7DQ8e7DJ5eEMi
https://x.com/i/grok/share/G53QXbgIdRcb5DqCerDT4qaFZ

让我们聊聊sourceless的调试(探针模式)

其实，静态类型就是在sourceless（无变量名）黑盒下的一种可观测性，它和模块划分、内存分配高度绑定
同时，类型也相当于一种“符号ID”，可以匹配不同版本、不同package里的相同代码
类型系统并不只是在“无源码做assert”或沟通API时起作用，它的本质是对程序行为的观测

这种观测可以延伸到runtime。即使对混淆过的控制流，不去推测其内部逻辑，只是hook平台的基础API（例如图层和键鼠函数），我们也能通过“指针污染”还原一定的逻辑
如果对基础API间组合关系的分析，能够进行codegen，并增量的patch到原有“汇编”，这就是动态分析的反混淆

九成情况下，AOP不是要完全获取source，而是要“理解”功能点间的联系，就像CheatEngine的数值搜索-锁定或A11y的检测点击一样。 安全界对此的认识到什么程度呢？ Ghidra,x64dbg,r2 都很好，但它们对程序似乎不是“语义化理解”，限于还原符号

我们不考虑二进制，或语言的AST或对象系统这些表象
type infer 究竟和这种“反混淆过程”多相似？

注意，二者都是在追溯已知“点”和“箭头”间的联系，从而推出新箭头乃至新点。

静态类型是用字面值的传导，推理箭头函数的形状，比如参数数量。在一个全部def均是SSA块(不含for,if)的代码树上，这一点非常明显。包含if或异常时它通过 union type 与类型变量，来更准确的表达点和箭头的联系。

动态分析是用污点返回值的传导，推理“箭头语句块”的流向，并探知新语句块的存在、新返回值的意图。

> libretro的接口是什么层次的？ 不会是一个ev/input+fb+sound 吧？还是，它负责类似MIDI的混合成？

简单来说，它就是个黑箱，类似 canvas+PCM+mouse/keyup ，图形没有层，只是bmp ……
tasvideos.org/Bizhawk 提供了完整的 mmap hook、PPU 寄存器、音频通道分离

#awesome
https://x.com/i/grok/share/i4YuHalu9C2pSaFpb6AgRTD7B
https://gist.github.com/aldelaro5/d532b21b5e2ec48d5f78e81846c1c1b7
https://github.com/michelhe/rustboyadvance-ng#:~:text=Incredible%20test%20suite
- https://felixjones.co.uk/mgba_gdb/vscode.html
- https://gbadev.net/tonc/setup.html

最开始是“RSC Payload 永远只能由可信的 React Server 产生，客户端必须 100% 信任它”
M1:{
"id": "../node_modules/malicious-module/index.js", // 路径越狱
"name": "default",
"chunks": [],
"children": [],
// 附加: 污染 prototype 让 eval 链起飞
"__proto__": { "require": "eval(maliciousCode)" }
}

Module Reference（指向服务器上的 JS 模块）
如果服务器在解析时没有严格校验 id 路径，或者有 prototype pollution 把 require cache 污染了，通过__flight__符号或类似机制，注入可执行的JS代码片段，就能加载任意模块。
某些旧版本的 React 真的把服务器组件的函数体序列化成字符串发下去（S: 开头），客户端直接 eval。

这波漏洞本质上就是：把“ hydration 需要执行的代码引用”当成普通数据传，结果在不可信环境里直接执行了。跟当年的 Java 反序列化、FastJSON @type
、Python pickle 是一个娘胎里出来的味儿。

我们用最复杂的Chromium做最简单的事（显示文字、在“单文件”内安全改变量名 ）
我们用最“先进”的流程拖慢一切（PR + CI + k8s + monorepo）
我们用最臃肿的方式打包最轻量的代码（3GB 镜像跑 2MB JS）
我们用最严格的安全扫描放行被误报的危险镜像（关扫描就完事了）
—— AI都明白