The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Suggesting to reply to this email is not a super idea because Coq-Club
automatically inserts a "reply-to" field set to 
coq-club AT inria.fr.
So I'd suggest instead that you give the e-mail address(es) to which
people interested to join the experiment should contact.

Cheers,
Théo

Le sam. 15 juin 2019 à 02:55, Talia Ringer 
<tringer AT cs.washington.edu>
 a écrit :
>
> 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