一句话：提出增量认证编程形式框架，定义完成精化与完备性，并在 Rocq 中实现 IncRease 原型。
认证编程通过证明助手和依赖类型语言同时定义规约与证明，保证软件满足需求，但部分定义和增量修改很容易破坏证明，因为规约通常没有考虑程序开发过程中的不完整状态。本文主张系统支持增量式认证编程，分析其目标与内在挑战，并提出形式框架。核心是定义完成精化（completion refinement）与完备性（completeness）来刻画增量性，并系统生成在开发各阶段均有效、同时保留原始陈述意图的规约。作者在 Rocq 证明助手中实现原型 IncRease，利用 typeclasses 实现自动化与可扩展性，且不依赖特定不完整处理机制。评估包括简单类型 λ 演算的增量教科书形式化，以及 CompCert 死代码消除优化 pass 的复杂案例；还展示与 QuickChick 随机性质测试兼容，并通过改编 Fiat 库研究其与演绎合成的结合。
Certified programming, as carried out in proof assistants and dependently-typed programming languages, ensures that a software meets its requirements by supporting the definition of both specifications and proofs. However, proofs easily break with partial definitions and incremental changes because specifications are not designed to account for the intermediate incomplete states of programs. We advocate for proper support for incremental certified programming by analyzing its objectives and inherent challenges, and propose a formal framework for achieving incremental certified programming in a principled manner. The key idea is to define appropriate notions of completion refinement and completeness to capture incrementality, and to systematically produce specifications that are valid at every stage of development while preserving the intent of the original statements. We provide a prototype implementation in the Rocq Prover, called IncRease, which exploits typeclasses for automation and extensibility, and is independent of any specific mechanism used to handle incompleteness. We illustrate its use with both an incremental textbook formalization of the simply-typed 𝜆-calculus, and a more complex case study of incremental certified programming for an existing dead-code elimination optimization pass of the CompCert project. We show that the approach is compatible with randomized property-based testing as provided by QuickChick. Finally we study how to combine incremental certified programming with deductive synthesis, using a novel incrementality-friendly adaptation of the Fiat library. This work provides theoretical and practical foundations towards systematic support for incremental certified programming, highlighting challenges and perspectives for future developments.
@article{paperbot2916,
title = {Incremental Certified Programming},
author = {Tomás Díaz and Kenji Maillard and Nicolas Tabareau and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763068}
}