Document Open Access Logo

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

Authors 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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.12.pdf
  • Filesize: 1.01 MB
  • 18 pages

Document Identifiers

Author Details

Ana de Almeida Borges
  • University of Barcelona, Spain
Annalí Casanueva Artís
  • Ifo Institut, München, Germany
Jean-Rémy Falleri
  • Univ. Bordeaux, Bordeaux INP, CNRS, UMR 5800 LaBRI, F-33400 Talence, Institut Universitaire de France, France
Emilio Jesús Gallego Arias
  • Université Paris Cité, CNRS, Inria, IRIF, F-75013, Paris, France
Érik Martin-Dorel
  • IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, France
Karl Palmskog
  • KTH Royal Institute of Technology, Stockholm, Sweden
Alexander Serebrenik
  • TU Eindhoven, The Netherlands
Théo Zimmermann
  • LTCI, Télécom Paris, Institut Polytechnique de Paris, France

Acknowledgements

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

Cite AsGet BibTex

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. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.12

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • General and reference → Empirical studies
Keywords
  • Coq
  • Community
  • Survey
  • Statistical Analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Ana de Almeida Borges, Jean-Rémy Falleri, Jim Fehrle, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Coq Community Survey 2022: Summary of Results, abstract. The Coq Workshop 2022, August 2022. URL: https://coq-workshop.gitlab.io/2022/abstracts/Coq2022-04-01-community-survey.pdf.
  2. Ana de Almeida Borges, Jean-Rémy Falleri, Jim Fehrle, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Coq Community Survey 2022: Summary of Results, slides. The Coq Workshop 2022, August 2022. URL: https://coq-workshop.gitlab.io/2022/slides/Coq2022-04-01-community-survey.pdf.
  3. Andrew W. Appel. Coq’s vibrant ecosystem for verification engineering (invited talk). In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pages 2-11, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3497775.3503951.
  4. Jasmin Christian Blanchette. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In International Conference on Certified Programs and Proofs, CPP 2019, pages 1-13, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294087.
  5. Thomas Braibant. Coq survey, 2014. URL: https://github.com/braibant/coq-survey/blob/master/popl-coq.pdf.
  6. Damian Clarke, Joseph P. Romano, and Michael Wolf. The Romano–Wolf multiple-hypothesis correction in Stata. The Stata Journal, 20(4):812-843, 2020. URL: https://doi.org/10.1177/1536867X20976314.
  7. The Coq Survey Working Group. Coq Community Survey 2022 in Chinese, 2022. URL: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/LimeSurvey/questionnaire_chinese.html.
  8. The Coq Survey Working Group. Coq Community Survey 2022 in English, 2022. URL: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/LimeSurvey/questionnaire_356388_en.html.
  9. The Coq Survey Working Group. Coq Community Survey 2022 Results: Part I (blog post), 2022. (Who is using Coq and in what context?). URL: https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730.
  10. The Coq Survey Working Group. Coq Community Survey 2022 Results: Part II (blog post), 2022. (How people are using Coq? - OS, IDEs, CI/CD). URL: https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746.
  11. The Coq Survey Working Group. Coq Community Survey 2022 Results: Part III (blog post), 2022. (How is Coq used? - features, tools, libraries). URL: https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777.
  12. 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. Supplementary material for the article "Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users", May 2023. URL: https://doi.org/10.5281/zenodo.7930567.
  13. Paul Duvall, Steve Matyas, and Andrew Glover. Continuous Integration: Improving Software Quality and Reducing Risk. Addison-Wesley Professional, first edition, 2007. Google Scholar
  14. Adrien Fabre. Tie-breaking the highest median: alternatives to the majority judgment. Social Choice and Welfare, 56(1):101-124, 2021. Google Scholar
  15. Taylor Fausak. State of Haskell survey, 2022. URL: https://taylor.fausak.me/2022/11/18/haskell-survey-results/.
  16. Sacha Greif and Eric Burel. State of JS, 2022. URL: https://2022.stateofjs.com/en-US/.
  17. Sture Holm. A simple sequentially rejective multiple test procedure. Scandinavian Journal of Statistics, 6(2):65-70, 1979. URL: http://www.jstor.org/stable/4615733.
  18. Glenn D Israel and CL Taylor. Can response order bias evaluations? Evaluation and Program Planning, 13(4):365-371, 1990. Google Scholar
  19. Mark L. Mitchell and Janina M. Jolley. Resarch Design Explained. Wadsworth, Cengage Learning, 7th edition, 2010. Google Scholar
  20. OCaml Software Foundation. OCaml user survey, 2020. URL: https://discuss.ocaml.org/t/suggestions-from-the-ocaml-survey-result/6791.
  21. OCaml Software Foundation. OCaml users survey, 2022. URL: https://ocaml-sf.org/docs/2022/ocaml-user-survey-2022.pdf.
  22. Stephen O'Grady. The RedMonk programming language rankings: June 2022, October 2022. URL: https://redmonk.com/sogrady/2022/10/20/language-rankings-6-22/.
  23. opam development team. OCaml package manager, 2023. URL: https://opam.ocaml.org.
  24. Karl Palmskog, Enrico Tassi, and Théo Zimmermann. Reliably reproducing machine-checked proofs with the Coq Platform. In Workshop on Reproducibility and Replication of Research Results, 2022. URL: https://arxiv.org/abs/2203.09835.
  25. Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2011. Japanese translation. URL: http://proofcafe.org/sf/.
  26. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Logical Foundations, volume 1 of Software Foundations. Electronic textbook, 2022. Chinese translation, version 5.7. URL: https://coq-zh.github.io/SF-zh/lf-current/index.html.
  27. Joseph P Romano and Michael Wolf. Stepwise multiple testing as formalized data snooping. Econometrica, 73(4):1237-1282, 2005. Google Scholar
  28. Stack Overflow. Stack Overflow developer survey, 2022. URL: https://survey.stackoverflow.co/2022/.
  29. The Coq Development Team. opam archive for Coq, 2023. URL: https://github.com/coq/opam-coq-archive.
  30. Mairieli Wessel, Alexander Serebrenik, Igor Wiese, Igor Steinmacher, and Marco A. Gerosa. What to expect from code review bots on GitHub? a survey with OSS maintainers. In Proceedings of the XXXIV Brazilian Symposium on Software Engineering, SBES '20, pages 457-462, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3422392.3422459.
  31. James R. Wilcox. Why is the Coq logo made to look like a penis?, April 2021. URL: https://sympa.inria.fr/sympa/arc/coq-club/2021-04/msg00006.html.
  32. Jeffrey M Wooldridge. Introductory econometrics: A modern approach. Cengage learning, 6th edition, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact