面向正确性设计的湖仓系统：数据契约、版本控制与事务性管道

湖仓（lakehouse）已成为分析和人工智能的默认存储子系统，但在并发且不可信的变更下仍然脆弱：模式不匹配往往仅在运行时显现，开发环境与生产环境容易 diverged，多表管道在失败后可能暴露部分结果。我们提出 Bauplan，一种面向正确性设计的代码驱动湖仓，旨在通过构造消除广泛的这些故障。Bauplan 基于已提供原子单表快照演化的存储子系统，增加了三种管道级正确性机制：类型化表契约以实现可检查的转换边界、类 Git 数据版本以支持可复现的协作与审阅，以及事务性运行以保证整个管道执行的原子发布。我们描述了系统设计，说明这些抽象如何整合到统一的编程模型中，以服务于人类和智能体，并报告了基于轻量级 Alloy 模型的早期结果，该模型既验证了关键直觉，也暴露了关于事务分支可见性的细微反例。我们的经验表明，湖仓的正确性最好不是通过事后修补故障来实现，而是通过限制编程模型，使得许多非法状态难以被表示。