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

Coq, community, survey, statistical analysis

Citation

de Almeida Borges, A., Casanueva Artís, A., Falleri, J.-R., Gallego Arias, E. J., Martin-Dorel, É., Palmskog, K., Serebrenik, A., & Zimmermann, T. (2023). Naumowicz, A. & Thiemann, R. (Eds.). Lessons for interactive theorem proving researchers from a survey of Coq users. 14th International Conference on Interactive Theorem Proving (ITP 2023) (pp. 12:1–12:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.12/LIPIcs.ITP.2023.12.pdf

@inproceedings{AlmeidaBorges2023_CoqSurvey,
  AUTHOR = "{de Almeida Borges}, Ana and {Casanueva Artís}, Annalí and Falleri, Jean-Rémy and {Gallego Arias}, Emilio Jesús and Martin-Dorel, Érik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Théo",
  EDITOR = "Naumowicz, Adam and Thiemann, René",
  TITLE = "Lessons for Interactive Theorem Proving Researchers from a Survey of {C}oq Users",
  BOOKTITLE = "14th International Conference on Interactive Theorem Proving (ITP 2023)",
  YEAR = "2023",
  ADDRESS = "Bialystok, Poland",
  PUBLISHER = "Schloss Dagstuhl -- Leibniz-Zentrum für Informatik",
  SERIES = "Leibniz International Proceedings in Informatics (LIPIcs)",
  VOLUME = "268",
  NUMBER = "22",
  PAGES = "12:1--12:18",
  URL = "https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.12/LIPIcs.ITP.2023.12.pdf",
  keywords = "Coq, community, survey, statistical analysis",
  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."
}