Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users

Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

6 Downloads (Pure)

Samenvatting

The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.

Originele taal-2Engels
Titel14th International Conference on Interactive Theorem Proving (ITP 2023)
RedacteurenAdam Naumowic, René Thiemann
UitgeverijSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Aantal pagina's18
ISBN van elektronische versie9783959772846, 978-3-95977-284-6
DOI's
StatusGepubliceerd - 26 jul. 2023
EvenementInteractive Theorem Proving - Białystok, Polen
Duur: 31 jul. 20234 aug. 2023
Congresnummer: 14
https://mizar.uwb.edu.pl/ITP2023/

Publicatie series

NaamLeibniz International Proceedings in Informatics (LIPIcs)
Volume268

Congres

CongresInteractive Theorem Proving
Verkorte titelITP
Land/RegioPolen
StadBiałystok
Periode31/07/234/08/23
Internet adres

Financiering

The authors would like to thank the survey participants, the Coq Survey Working Group members who are not simultaneously authors of this paper (Yves Bertot, Nathan Cassee, Jim Fehrle, Jerome Hugues, Barry Jay, Matthieu Sozeau and Enrico Tassi), the survey beta testers, and the translator team (Yishuai Li, Oling Cat and Weidu Kuang).

Vingerafdruk

Duik in de onderzoeksthema's van 'Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users'. Samen vormen ze een unieke vingerafdruk.

Citeer dit