The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hello Coq users,

We (Talia Ringer and Alex Sanchez-Stern , Ph.D. students at UW and UCSD respectively) are working on a study to investigate the development processes of proof engineers. Right now, we are looking for some beta testers for a simple reporting plugin we've developed to analyze these development processes. Data from this round will be discarded, but your feedback on the plugin will help us refine the tool and eventually collect and analyze data that will have broad applications for the Coq community and for the ITP community more broadly. Please see below for details, and please contact us if you are interested or if you have any questions.

Best,

Talia and Alex

---

Motivation: In recent years, verification efforts using interactive theorem provers like Coq have reached large, critical software projects. Unfortunately, while there is a lot of available data on completed proof projects, there is little data on the development processes of proof engineers. We have developed a Coq plugin that collects data on the changes that proof engineers make in development, so that we can later analyze this data.

Where you can help: We're looking for volunteers to install this plugin and use it during their proof development for a period of two weeks, so that we can work out any bugs in the collection process before our study. Eventually, we plan to deploy to a larger group of users and analyze the resulting development data, then use it to inform the next generation of proof automation tooling.

How to help: This is only a beta test of the infrastructure, so the data collected in this phase will be discarded. However, we'll also contact you about joining the full study (if you are interested) after the beta period has ended.

Should you choose to join our beta test, your duties will be as follows:

• Install our plugin
  
• Load our plugin before working on developments (there is a way to do this just once)
• Use Coq master branch for development with our plugin for a period of two weeks
  
• Report any bugs you encounter

Benefits: We anticipate that our work will benefit the broader community of proof engineers, and we plan to make the eventual dataset publicly available. We will also use the data to write a paper on the habits and processes of proof engineers, as well as to inform the development of tools for automated proof repair and machine learning for proof automation so that these tools meet the needs of real proof engineers like you.

How to join: If you're interested in joining this beta test, please reply (not reply all) to this email, and we will contact you with further steps. Please also let us know if you have any questions.

Thanks,

Talia and Alex