We (Talia Ringer and Alex Sanchez-Stern , Ph.D. students at UW and UCSD respectively) are recruiting proof engineers to participate in a study of the development processes of proof engineers in Coq. Please see the following video: https://www.youtube.com/watch?v=JzoRNwBPyGo
This study will help inform the design of future proof automation tooling, and will be useful to the community more broadly. If you are interested, please fill out this screening survey and we will be in touch if you are eligible. The full study description is below, as well as in the video description.
Please spread the word, and thanks!
Talia and Alex
In recent years, verification efforts using proof assistants like like Coq have reached large, critical software projects. In spite of this, there is little data on the development processes of proof engineers. We are deploying a Coq plugin to a group of proof engineers that collects data on the changes that proof engineers make in development, then analyzing the data and using it to inform the next generation of proof automation tooling.
Getting Involved
If you are interested in participating, please fill out this screening survey and we will be in touch if you are eligible. Filling out this survey is not a commitment to participate.
The only requirements to get involved are that you are 18 years or older, fluent in English, and have at least a year of experience using the Coq proof assistant.
Study Details
During the study, we will send you a link to install our Coq plugin. To install this plugin, you will need a recent version of Coq. You may use any editor or development environment. The plugin will ask you a few questions about your background and development environment the first time you install it.
After that, we will ask you to continue normal Coq development with the plugin installed for a period of one month, running from August 7th through September 7th. The plugin will collect data on the changes that you make in development, which we will later analyze.
Data Details
If you choose to participate, we will collect your name and email address for screening purposes and for later contact; this information will not be linked to the study data or to any publications.
The plugin will collect the changes that you make to Coq developments, including changes to definitions and proofs, as well as how you step through the file interactively. The plugin will assign you a unique identifier and store this data linked to that unique identifier in a server.
We will analyze the resulting data and use the results of our analysis to write a research paper on the development practices of proof engineers in Coq. We will also use the results of our analysis to inform the design of a proof patching tool and of a machine learning tool for tactics. We will also release the data for use in other research.
If you choose to participate, we will send you a consent form with more details.
Benefits
We anticipate that our work will benefit the broader community of proof engineers, and we plan to make the dataset publicly available. We will also use the data to write a paper on the 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.