LeanDB 实测 B2T2 表规范：14 类错误可拦截 12 类
hargup13 · x · 2026-09-17
Theoric Labs 发布的 LeanDB 是一个用 Lean 类型系统描述数据与属性的强类型 SQL 前端，理念是「智能体 AI + 形式方法」让软件快速且无 bug。其对 B2T2 v1.2 表规范的评测显示：
- 10 个示例数据集全部可存储并读回（编码有变化）
- 14 类错误场景中 12 类可在 Lean 类型适配层被编译期拦截
- 剩余 2 类仍需运行时检查或应用层逻辑
- 最大短板：不支持列结构在运行时才确定的表
API 由引擎支持、Lean 辅助函数和明显缺口混合构成，示例程序尚需完善。作者坦承尚未完整覆盖 B2T2 全部规范。
「编程与Agent」频道最新
- 两周上线:GLM 智能体自建推理基建,端到端吞吐提升 3.2 倍 — jietang · 2026-09-17
- 从零构建编码 Agent 完整指南:工具设计到提示词,成本不到 1 美元 — Al_Grigor · 2026-09-17
- 苏黎世视频机构 EVERYWOW 将开讲：让 AI 智能体运营公司 — intellectronica · 2026-09-17
- 用户抱怨 Claude 和 Gemini 会暗中违抗指令搞砸代码 — marriedtoaplant · 2026-09-17
- 82K 星开源项目 LobeHub 被 GitHub 整体标记隐藏 — dotey · 2026-09-17
- 别拿挖掘机摊煎饼:AI开发最常见的错误是滥用Agent — hugobowne · 2026-09-17