Abstract
Proof engineering tools make it easier to develop and maintain large systems verified using interactive theorem provers. Developing useful proof engineering tools hinges on understanding the development processes of proof engineers. This paper breaks down one barrier to achieving that understanding: remotely collecting granular data on proof developments as they happen. We have built a tool called REPLica that instruments Coq's interaction model in order to collect fine-grained data on proof developments. It is decoupled from the user interface, and designed in a way that generalizes to other interactive theorem provers with similar interaction models. We have used REPLica to collect data over the span of a month from a group of intermediate through expert proof engineers-enough data to reconstruct hundreds of interactive sessions. The data reveals patterns in fixing proofs and in changing programs and specifications useful for the improvement of proof engineering tools. Our experiences conducting this study suggest design considerations both at the level of the study and at the level of the interactive theorem prover that can facilitate future studies of this kind.
Original language | English (US) |
---|---|
Title of host publication | CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020 |
Editors | Jasmin Blanchette, Catalin Hritcu |
Publisher | Association for Computing Machinery, Inc |
Pages | 99-113 |
Number of pages | 15 |
ISBN (Electronic) | 9781450370974 |
DOIs | |
State | Published - Jan 20 2020 |
Externally published | Yes |
Event | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States Duration: Jan 20 2020 → Jan 21 2020 |
Conference
Conference | 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 |
---|---|
Country/Territory | United States |
City | New Orleans |
Period | 1/20/20 → 1/21/20 |
Keywords
- Proof engineering
- Study methodologies
- User interaction
ASJC Scopus subject areas
- Computer Science Applications
- Software