TY - GEN
T1 - Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
AU - de Almeida Borges, Ana
AU - Artís, Annalí Casanueva
AU - Falleri, Jean Rémy
AU - Arias, Emilio Jesús Gallego
AU - Martin-Dorel, Érik
AU - Palmskog, Karl
AU - Serebrenik, Alexander
AU - Zimmermann, Théo
N1 - Publisher Copyright:
© Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann; licensed under Creative Commons License CC-BY 4.0 14th International Conference on Interactive Theorem Proving (ITP 2023)
PY - 2023/7/1
Y1 - 2023/7/1
N2 - 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.
AB - 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.
KW - Community
KW - Coq
KW - Statistical Analysis
KW - Survey
U2 - 10.4230/LIPIcs.ITP.2023.12
DO - 10.4230/LIPIcs.ITP.2023.12
M3 - Conference contribution
AN - SCOPUS:85168761707
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 14th International Conference on Interactive Theorem Proving, ITP 2023
A2 - Naumowicz, Adam
A2 - Thiemann, Rene
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 14th International Conference on Interactive Theorem Proving, ITP 2023
Y2 - 31 July 2023 through 4 August 2023
ER -