One Seattle summer day, a proof engineer is struggling to get his Coq proofs to go through. Together with heroes The Eliminator and The Tactician, he devises a plan to help not just himself, but the Coq community more broadly. In doing so, he, too, becomes a hero.
His plan is to help contribute his data to the Coq Change Analytics study. You can join him, and become a hero too. (We'll give you a superhero name if you want one.) If you are interested, please fill out this screening survey: We will be in touch if you are eligible. The full study description is below.
---
Study Description
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 at 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.
---
Cast & Crew
Narrator: Dimitar Bounov, UCSD Alumnus
Proof engineer/Mr. QED: Martin Kellogg, UW
Friend: Chandrakana Nandi, UW
The Eliminator: Talia Ringer, UW
The Tactician: Alex Sanchez-Stern, UCSD
Director: Talia Ringer, UW
Filming: Doug Woos, UW Alumnus
Video Editing: Alex Sanchez-Stern, UCSD
Pun Consultants: Karl Palmskog, UT Austin & Dan Grossman, UW
Has laoreet percipitur ad. Vide interesset in mei, no his legimus verterem. Et nostrum imperdiet appellantur usu, mnesarchum referrentur id vim.
0 comments:
Post a Comment