不要调用我们，我们会调用你：迈向面向编程语言理论的混合主动交互式证明助手

编程语言研究人员在工作中使用两类系统。语义工程工具允许他们交互式地探索其定义，而证明助手可用于检查其属性证明。这两类系统之间的脱节导致了已发表论文中的错误，也限制了在编写证明时可用的交互模式。在构建证明时，通常先陈述属性，然后手动开发证明，直到自动策略能够填补剩余空白。我们相信，一种利用编程语言典型结构的集成且更具交互性的工具可以做得更好。一个了解编程语言证明典型结构的证明助手可能需要更少的人工输入，帮助用户理解他们的证明，同时还能在证明构建中使用来自可执行语义探索的见解。在本文提出的早期工作中，我们关注与证明助手交互的问题，而将语义工程部分留待未来解决。我们提出了一种工作方式，不是从手动构建证明开始然后自动完成最后步骤，而是工具从自动证明搜索开始，然后在需要用户反馈时中断。我们构建了一个遵循这种交互模式的小型证明助手，并使用 Peano 算术中“+”操作交换律的简单证明说明了该想法。我们的早期经验表明，这种工作方式可以使证明构建更容易。