We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype implementation.

翻译：本文提出为Dafny系统扩展交互式证明模式。我们通过一个启发性示例，阐述交互式证明模式的工作原理，包括核心设计决策，并展示原型实现方案。