Don't Call Us, We'll Call You: Towards Mixed-Initiative Interactive Proof Assistants for Programming Language Theory

TL;DR

This paper proposes a mixed-initiative proof assistant for programming language theory that combines automatic proof search with user interaction, aiming to make proof development more intuitive and less error-prone.

Contribution

It introduces a novel interaction mode where the proof assistant begins with automatic proof search and seeks user feedback when needed, enhancing proof construction.

Findings

Proof assistant starts with automatic proof search.

User feedback guides proof development.

Initial implementation simplifies proof construction.

Abstract

There are two kinds of systems that programming language researchers use for their work. Semantics engineering tools let them interactively explore their definitions, while proof assistants can be used to check the proofs of their properties. The disconnect between the two kinds of systems leads to errors in accepted publications and also limits the modes of interaction available when writing proofs. When constructing a proof, one typically states the property and then develops the proof manually until an automatic strategy can fill the remaining gaps. We believe that an integrated and more interactive tool that leverages the typical structure of programming language could do better. A proof assistant aware of the typical structure of programming language proofs could require less human input, assist the user in understanding their proofs, but also use insights from the exploration of executable semantics in proof construction. In the early work presented in this paper, we focus on the problem of interacting with a proof assistant and leave the semantics engineering part to the future. Rather than starting with manual proof construction and then completing the last steps automatically, we propose a way of working where the tool starts with an automatic proof search and then breaks when it requires feedback from the user. We build a small proof assistant that follows this mode of interaction and illustrates the idea using a simple proof of the commutativity of the "+" operation for Peano arithmetic. Our early experience suggests that this way of working can make proof construction easier.