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 (IDEs).
Authors
- Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806)
- Karl Palmskog
- Ana de Almeida Borges (ORCID: https://orcid.org/0000-0001-5152-198X)
- Érik Martin-Dorel (ORCID: https://orcid.org/0000-0001-9716-9491)
- Alexander Serebrenik (ORCID: https://orcid.org/0000-0002-1418-0095)
- Emilio Jesús Gallego Arias (ORCID: https://orcid.org/0000-0002-9299-1192)
- Jean‐Rémy Falleri (ORCID: https://orcid.org/0000-0002-8284-7218)
- Annalí Casanueva Artís
Institutions
- Centre National de la Recherche Scientifique (FR)
- Ifo Institute for Economic Research (DE)
- Université Toulouse III - Paul Sabatier (FR)
- Université de Bordeaux (FR)
- Université Fédérale de Toulouse Midi-Pyrénées (FR)
- Institut Universitaire de France (FR)
- Université Paris Cité (FR)
- Université Toulouse-I-Capitole (FR)
- Institut de Recherche en Informatique de Toulouse (FR)
- Laboratoire Bordelais de Recherche en Informatique (FR)
- Institut Polytechnique de Paris (FR)
- Embedded Systems (United States) (US)
- Université Toulouse - Jean Jaurès (FR)
- Institut Polytechnique de Bordeaux (FR)
- Laboratoire Traitement et Communication de l’Information (FR)
- Universitat de Barcelona (ES)
- Eindhoven University of Technology (NL)
- KTH Royal Institute of Technology (SE)
Publication Details
- Journal
- Journal of Automated Reasoning
- Published
- 2025-02-20
- DOI
- https://doi.org/10.1007/s10817-025-09720-1
- Primary Topic
- Distributed and Parallel Computing Systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Stiftelsen för Strategisk Forskning
- Kungliga Tekniska Högskolan