Abstract:
Proof assistants gained momentum in the past decade. The popularization of functional programming and the rise of industry cases using formal verification contributed to the popularity growth of Coq, Lean, Agda, and other related projects. However, the existing tools for writing proofs in most of these assistants are limited. There is almost no record of usability and interface studies for tools targeting the development of proofs. After presenting a survey on the plug-ins and standalone working interfaces for Coq and Lean, this work introduces a proposal for a data-centered user study to improve the existing development environments for proof assistants. We will also explore a few features that would decrease the entry-bar for Coq, potentially helping students and even experienced users.
PPIG 2021 - 32nd Annual Workshop
A Data-Centered User Study for Proof Assistant Tools