Hydro 用形式化验证检查分布式算子交换律证明
ShadajL · x · 2026-09-23
Shadaj 在 hydro-project 合并 PR #3198，为 Hydro 语言的 commutative = ... 注解引入基于 Verus 的机器检验证明，作为手动证明的替代。证明义务由宏从闭包体自动生成，用户无需手写断言，且按算子形状分别生成：
- fold/reduce：证明两种顺序下最终累加器相等
- map：证明捕获状态相等、输出多重集相等（能抓住运行总数这类暴露顺序的输出）
- filter：证明捕获状态相等、保留元素多重集相等
这项工作基于 Conor Power 的博士论文研究——不依赖 LLM 写出正确的规约，就能在分布式系统中用形式化验证替代信任。
「编程与Agent」频道最新
- Claude Code 编排工具 ao 用户破万,创始人加入旧金山 Solo Founders Programme — julianweisser · 2026-09-24
- 工程师吐槽 vibe coding:按钮上出现错误的 aria-checked 属性 — jh3yy · 2026-09-24
- serve-sim 新版支持 iPhone Duo:3D 模拟器+agent 检查无障碍树 — Baconbrix · 2026-09-24
- 开源 Nautilo 推出可指挥 Codex 与 Claude Code 的上层 Agent — Dan_Jeffries1 · 2026-09-24
- LangChain 给 Managed Deep Agents 加 cron 定时任务,Agent 可自主运行 — LangChain · 2026-09-24
- Vercel Sandbox 推出持久存储 Drives:单盘最大 16 TiB,写速度达 NVMe — cramforce · 2026-09-24