正在打开每日关注
正在打开每日关注
把 Haskell 的 GDP 模式移植到 TypeScript，编译期验证授权证明，防止人与 Agent 写出越权漏洞。
Introducing gdp-ts: Ghosts of Departed Proofs for TypeScript. gdp-ts is a library, linter and AI skill for safer API design. Under this contract, sensitive functions require 'proofs' that the caller performed an authorization check. The typechecker verifies these proofs at compile time, preventing your team and agents from shipping catastrophic security (and other kinds of) bugs. While these patterns have existed for quite some time, especially in ecosystems like Haskell, ① human code review and ② cognitive and syntactic overhead made these solutions niche. The situation is now inverted. Agents are writing more code than we can review, and they *thrive* in tight loops with hard constraints that would frustrate us. We see this with the rise of Rust, borrow checker, code aesthetics debate and all. The README and examples model a real-world Vercel API product constraint: changing the password on a Project requires a proof of a certain role + a certain entitlement. Thanks to Matt Noonan and Ollie Charles for their research in this space. https://t.co/eRWdiMvQ2V
是什么：rauchg 发布的 gdp-ts 是 Haskell "Ghosts of Departed Proofs" 模式的 TypeScript 实现，三件套形态：@gdp-ts/core 库、ESLint/Oxlint 预设，以及通过 npx skills add 安装、指导编码 Agent 的 AI Skill。仓库 701 星，要求 TS 5.4+，示例以 Vercel 密码保护为原型。
核心设计：三步闭环——name() 给运行时值一个编译期名字；只有 proofs/ 下的可信模块能铸造 Proof；敏感函数在签名中要求关于同一具体值的证明，缺证明、错证明或传裸 id 都无法编译。证明是"幽灵"，运行时只是冻结的 {kind} 对象，几乎零开销；as 伪造等漏洞交给 lint 拦截。
关键洞察：GDP 模式过去小众，是因为人工审查扛不住认知与语法负担；而 Agent 恰好在"硬约束+紧密反馈循环"里表现最好。把授权从口头约定升级为类型无法绕过的契约，等于把安全审查前移到编译期，正中 Agent 时代痛点。数据层因要求证明而可安全导出，路由、Server Action、定时任务都跳不过检查。
边界与风险：README 明确不防运行时绕过与陈旧证明（检查后角色可能变化）；严格度是"易用-严格滑块"，需按风险取舍；与 CASL 等策略引擎互补而非替代；类型检查成本随调用点线性增长（约 0.3ms/点）。