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

doi:10.4230/LIPIcs.ITP.2023.12

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

Software Engineering and Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

41 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	14th International Conference on Interactive Theorem Proving (ITP 2023)
Editors	Adam Naumowic, René Thiemann
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages	18
ISBN (Electronic)	9783959772846, 978-3-95977-284-6
DOIs	https://doi.org/10.4230/LIPIcs.ITP.2023.12
Publication status	Published - 26 Jul 2023
Event	Interactive Theorem Proving - Białystok, Poland Duration: 31 Jul 2023 → 4 Aug 2023 Conference number: 14 https://mizar.uwb.edu.pl/ITP2023/

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Volume	268

Conference

Conference	Interactive Theorem Proving
Abbreviated title	ITP
Country/Territory	Poland
City	Białystok
Period	31/07/23 → 4/08/23
Internet address	https://mizar.uwb.edu.pl/ITP2023/

Funding

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).

Keywords

Community
Coq
Statistical Analysis
Survey

Access to Document

10.4230/LIPIcs.ITP.2023.12

pdfFinal published version, 1.02 MBLicence: CC BY

Cite this

de Almeida Borges, A., Casanueva Artís, A., Falleri, J.-R., Gallego Arias, E. J., Martin-Dorel, É., Palmskog, K., Serebrenik, A., & Zimmermann, T. (2023). Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In A. Naumowic, & R. Thiemann (Eds.), 14th International Conference on Interactive Theorem Proving (ITP 2023) (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 268). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITP.2023.12

de Almeida Borges, Ana ; Casanueva Artís, Annalí ; Falleri, Jean-Rémy et al. / Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. 14th International Conference on Interactive Theorem Proving (ITP 2023) . editor / Adam Naumowic ; René Thiemann. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{a822e9c90d03463aac614c50ce4614f8,

title = "Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users",

abstract = "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.",

keywords = "Community, Coq, Statistical Analysis, Survey",

author = "\{de Almeida Borges\}, Ana and \{Casanueva Art{\'i}s\}, Annal{\'i} and Jean-R{\'e}my Falleri and \{Gallego Arias\}, \{Emilio Jes{\'u}s\} and {\'E}rik Martin-Dorel and Karl Palmskog and Alexander Serebrenik and Th{\'e}o Zimmermann",

year = "2023",

month = jul,

day = "26",

doi = "10.4230/LIPIcs.ITP.2023.12",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

editor = "Adam Naumowic and Ren{\'e} Thiemann",

booktitle = "14th International Conference on Interactive Theorem Proving (ITP 2023)",

note = "Interactive Theorem Proving, ITP ; Conference date: 31-07-2023 Through 04-08-2023",

url = "https://mizar.uwb.edu.pl/ITP2023/",

}

de Almeida Borges, A, Casanueva Artís, A, Falleri, J-R, Gallego Arias, EJ, Martin-Dorel, É, Palmskog, K, Serebrenik, A & Zimmermann, T 2023, Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. in A Naumowic & R Thiemann (eds), 14th International Conference on Interactive Theorem Proving (ITP 2023) . Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Interactive Theorem Proving, Białystok, Poland, 31/07/23. https://doi.org/10.4230/LIPIcs.ITP.2023.12

Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. / de Almeida Borges, Ana; Casanueva Artís, Annalí; Falleri, Jean-Rémy et al.
14th International Conference on Interactive Theorem Proving (ITP 2023) . ed. / Adam Naumowic; René Thiemann. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 268).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - de Almeida Borges, Ana

AU - Casanueva Artís, Annalí

AU - Falleri, Jean-Rémy

AU - Gallego Arias, Emilio Jesús

AU - Martin-Dorel, Érik

AU - Palmskog, Karl

AU - Serebrenik, Alexander

AU - Zimmermann, Théo

N1 - Conference code: 14

PY - 2023/7/26

Y1 - 2023/7/26

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

UR - https://www.scopus.com/pages/publications/85168761707

U2 - 10.4230/LIPIcs.ITP.2023.12

DO - 10.4230/LIPIcs.ITP.2023.12

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

BT - 14th International Conference on Interactive Theorem Proving (ITP 2023)

A2 - Naumowic, Adam

A2 - Thiemann, René

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - Interactive Theorem Proving

Y2 - 31 July 2023 through 4 August 2023

ER -

de Almeida Borges A, Casanueva Artís A, Falleri JR, Gallego Arias EJ, Martin-Dorel É, Palmskog K et al. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In Naumowic A, Thiemann R, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023) . Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2023. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.ITP.2023.12

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

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this