{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T04:23:00Z","timestamp":1742703780593,"version":"3.40.2"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T00:00:00Z","timestamp":1740009600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T00:00:00Z","timestamp":1740009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001729","name":"Stiftelsen f\u00f6r\u00a0Strategisk Forskning","doi-asserted-by":"publisher","award":["Trustfull"],"award-info":[{"award-number":["Trustfull"]}],"id":[{"id":"10.13039\/501100001729","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004270","name":"Royal Institute of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004270","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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).<\/jats:p>","DOI":"10.1007\/s10817-025-09720-1","type":"journal-article","created":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T17:46:46Z","timestamp":1740073606000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users"],"prefix":"10.1007","volume":"69","author":[{"given":"Ana","family":"de Almeida Borges","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annal\u00ed","family":"Casanueva Art\u00eds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-R\u00e9my","family":"Falleri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emilio Jes\u00fas","family":"Gallego Arias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Palmskog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Serebrenik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Th\u00e9o","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,20]]},"reference":[{"key":"9720_CR1","unstructured":"Greif, S., Burel, E.: State of JS (2022). https:\/\/2022.stateofjs.com\/en-US\/"},{"key":"9720_CR2","unstructured":"Stack Overflow: Stack Overflow Developer Survey (2022). https:\/\/survey.stackoverflow.co\/2022\/"},{"key":"9720_CR3","doi-asserted-by":"publisher","unstructured":"Wessel, M., Serebrenik, A., Wiese, I., Steinmacher, I., Gerosa, M.A.: 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 \u201920, pp. 457\u2013462. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3422392.3422459","DOI":"10.1145\/3422392.3422459"},{"key":"9720_CR4","unstructured":"O\u2019Grady, S.: The RedMonk Programming Language Rankings: June 2022 (2022). https:\/\/redmonk.com\/sogrady\/2022\/10\/20\/language-rankings-6-22\/"},{"key":"9720_CR5","unstructured":"Braibant, T.: Coq survey (2014). https:\/\/github.com\/braibant\/coq-survey\/blob\/master\/popl-coq.pdf"},{"key":"9720_CR6","unstructured":"LimeSurvey Developers: LimeSurvey (2024). https:\/\/www.limesurvey.org"},{"key":"9720_CR7","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Coq\u2019s vibrant ecosystem for verification engineering (invited talk). In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022, pp. 2\u201311. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3497775.3503951","DOI":"10.1145\/3497775.3503951"},{"key":"9720_CR8","unstructured":"Wilcox, J.R.: Why is the Coq logo made to look like a penis? (2021). https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2021-04\/msg00006.html"},{"key":"9720_CR9","unstructured":"The Coq Survey Working Group: Coq Community Survey 2022 in English (2022). https:\/\/thzimmer.gitlabpages.inria.fr\/coq-survey-2022-assets\/LimeSurvey\/questionnaire_356388_en.html"},{"key":"9720_CR10","unstructured":"The Coq Survey Working Group: Coq Community Survey 2022 in Chinese (2022). https:\/\/thzimmer.gitlabpages.inria.fr\/coq-survey-2022-assets\/LimeSurvey\/questionnaire_chinese.html"},{"key":"9720_CR11","unstructured":"The Coq Survey Working Group: Coq Community Survey 2022 Results: Part I (blog post). (Who is using Coq and in what context?) (2022). https:\/\/coq.discourse.group\/t\/coq-community-survey-2022-results-part-i\/1730"},{"key":"9720_CR12","unstructured":"The Coq Survey Working Group: Coq Community Survey 2022 Results: Part II (blog post). (How people are using Coq?\u2014OS, IDEs, CI\/CD) (2022). https:\/\/coq.discourse.group\/t\/coq-community-survey-2022-results-part-ii\/1746"},{"key":"9720_CR13","unstructured":"The Coq Survey Working Group: Coq Community Survey 2022 Results: Part III (blog post). (How is Coq used?\u2014features, tools, libraries) (2022). https:\/\/coq.discourse.group\/t\/coq-community-survey-2022-results-part-iii\/1777"},{"key":"9720_CR14","unstructured":"de Almeida Borges, A., Falleri, J.-R., Fehrle, J., Gallego\u00a0Arias, E.J., Martin-Dorel, \u00c9., Palmskog, K., Serebrenik, A., Zimmermann, T.: Coq Community Survey 2022: Summary of Results, abstract. The Coq Workshop 2022 (2022). https:\/\/coq-workshop.gitlab.io\/2022\/abstracts\/Coq2022-04-01-community-survey.pdf"},{"key":"9720_CR15","unstructured":"de Almeida Borges, A., Falleri, J.-R., Fehrle, J., Gallego\u00a0Arias, E.J., Martin-Dorel, \u00c9., Palmskog, K., Serebrenik, A., Zimmermann, T.: Coq Community Survey 2022: Summary of Results, slides. The Coq Workshop 2022 (2022). https:\/\/coq-workshop.gitlab.io\/2022\/slides\/Coq2022-04-01-community-survey.pdf"},{"key":"9720_CR16","doi-asserted-by":"publisher","unstructured":"Almeida\u00a0Borges, A., Casanueva\u00a0Art\u00eds, A., Falleri, J.-R., Gallego\u00a0Arias, E.J., Martin-Dorel, E., Palmskog, K., Serebrenik, A., Zimmermann, T.: Lessons for interactive theorem proving researchers from a survey of Coq users. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, pp. 12\u201311218. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.12","DOI":"10.4230\/LIPIcs.ITP.2023.12"},{"key":"9720_CR17","unstructured":"Coq Survey Working Group, T.: Coq Community Survey 2022 Results: Part IV (blog post). (Improvements to Coq, contributing to Coq, community health, and renaming Coq) (2023). https:\/\/coq.discourse.group\/t\/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement\/2001"},{"key":"9720_CR18","unstructured":"Fausak, T.: State of Haskell Survey (2022). https:\/\/taylor.fausak.me\/2022\/11\/18\/haskell-survey-results\/"},{"key":"9720_CR19","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7930567","author":"A de Almeida Borges","year":"2023","unstructured":"de Almeida Borges, A., Casanueva Art\u00eds, A., Falleri, J.-R., Gallego Arias, E.J., Martin-Dorel, \u00c9., Palmskog, K., Serebrenik, A., Zimmermann, T.: Supplementary material for the article \u201clessons for interactive theorem proving researchers from a survey of Coq users\u2019\u2019. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7930567","journal-title":"Zenodo"},{"key":"9720_CR20","unstructured":"OCaml Software Foundation: OCaml User Survey (2020). https:\/\/discuss.ocaml.org\/t\/suggestions-from-the-ocaml-survey-result\/6791"},{"key":"9720_CR21","volume-title":"Research Design Explained","author":"ML Mitchell","year":"2010","unstructured":"Mitchell, M.L., Jolley, J.M.: Research Design Explained, 7th edn. Cengage Learning, Wadsworth (2010)","edition":"7"},{"key":"9720_CR22","unstructured":"Pierce, B.C., Amorim, A.A., Casinghino, C., Gaboardi, M., Greenberg, M., Hri\u0163cu, C., Sj\u00f6berg, V., Yorgey, B.: Logical Foundations. Software Foundations, vol. 1. Electronic textbook, Online (2022). Chinese translation, version 5.7. https:\/\/coq-zh.github.io\/SF-zh\/lf-current\/index.html"},{"key":"9720_CR23","unstructured":"Pierce, B.C., Casinghino, C., Greenberg, M., Sj\u00f6berg, V., Yorgey, B.: Software Foundations. Electronic textbook, Online (2011). Japanese translation. http:\/\/proofcafe.org\/sf\/. Accessed 27 May 2024"},{"key":"9720_CR24","unstructured":"TYPES community: Types-announce mailing list (2024). https:\/\/lists.seas.upenn.edu\/mailman\/listinfo\/types-announce"},{"key":"9720_CR25","unstructured":"GDR IM: GDR IM (Informatics and Mathematics National Working Group) mailing list (2024). https:\/\/mail.gdr-im.fr\/sympa"},{"key":"9720_CR26","unstructured":"GDR GPL: GDR GPL (Software and Programming National Working Group) mailing list (2024). https:\/\/listes.univ-grenoble-alpes.fr\/sympa\/info\/gdr.gpl"},{"key":"9720_CR27","unstructured":"Project Jupyter: Jupyter (2024). https:\/\/jupyter.org"},{"key":"9720_CR28","unstructured":"StataCorp: Stata (2024). https:\/\/www.stata.com"},{"key":"9720_CR29","volume-title":"Introductory Econometrics: A Modern Approach","author":"JM Wooldridge","year":"2015","unstructured":"Wooldridge, J.M.: Introductory Econometrics: A Modern Approach, 6th edn. Cengage Learning, Mason (2015)","edition":"6"},{"issue":"4","key":"9720_CR30","doi-asserted-by":"publisher","first-page":"1237","DOI":"10.1111\/j.1468-0262.2005.00615.x","volume":"73","author":"JP Romano","year":"2005","unstructured":"Romano, J.P., Wolf, M.: Stepwise multiple testing as formalized data snooping. Econometrica 73(4), 1237\u20131282 (2005)","journal-title":"Econometrica"},{"issue":"4","key":"9720_CR31","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1177\/1536867X20976314","volume":"20","author":"D Clarke","year":"2020","unstructured":"Clarke, D., Romano, J.P., Wolf, M.: The Romano-Wolf multiple-hypothesis correction in Stata. Stata J. 20(4), 812\u2013843 (2020). https:\/\/doi.org\/10.1177\/1536867X20976314","journal-title":"Stata J."},{"issue":"2","key":"9720_CR32","first-page":"65","volume":"6","author":"S Holm","year":"1979","unstructured":"Holm, S.: A simple sequentially rejective multiple test procedure. Scand. J. Stat. 6(2), 65\u201370 (1979)","journal-title":"Scand. J. Stat."},{"key":"9720_CR33","unstructured":"OCaml Software Foundation: OCaml Users Survey (2022). https:\/\/ocaml-sf.org\/docs\/2022\/ocaml-user-survey-2022.pdf"},{"key":"9720_CR34","doi-asserted-by":"publisher","unstructured":"Palmskog, K., Tassi, E., Zimmermann, T.: Reliably reproducing machine-checked proofs with the Coq Platform. In: Workshop on Reproducibility and Replication of Research Results (2022). https:\/\/doi.org\/10.48550\/arXiv.2203.09835","DOI":"10.48550\/arXiv.2203.09835"},{"issue":"CSCW1","key":"9720_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3449218","volume":"5","author":"R Li","year":"2021","unstructured":"Li, R., Pandurangan, P., Frluckaj, H., Dabbish, L.: Code of conduct conversations in open source software projects on Github. Proc. ACM Hum. Comput. Interact. 5(CSCW1), 1\u201331 (2021)","journal-title":"Proc. ACM Hum. Comput. Interact."},{"key":"9720_CR36","doi-asserted-by":"crossref","unstructured":"Robson, N.: Diversity and decorum in open source communities. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 986\u2013987 (2018)","DOI":"10.1145\/3236024.3275441"},{"key":"9720_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-020-09543-w","author":"V Singh","year":"2021","unstructured":"Singh, V., Bongiovanni, B., Brandon, W.: Codes of conduct in Open Source Software\u2014for warm and fuzzy feelings or equality in community? Softw. Qual. J. (2021). https:\/\/doi.org\/10.1007\/s11219-020-09543-w","journal-title":"Softw. Qual. J."},{"key":"9720_CR38","doi-asserted-by":"crossref","unstructured":"Tourani, P., Adams, B., Serebrenik, A.: Code of conduct in open source projects. In: 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER), pp. 24\u201333. IEEE (2017)","DOI":"10.1109\/SANER.2017.7884606"},{"key":"9720_CR39","unstructured":"opam development team: OCaml Package Manager (2023). https:\/\/opam.ocaml.org"},{"key":"9720_CR40","unstructured":"The Coq Development Team: opam archive for Coq (2023). https:\/\/github.com\/coq\/opam-coq-archive"},{"key":"9720_CR41","volume-title":"Continuous Integration: Improving Software Quality and Reducing Risk","author":"P Duvall","year":"2007","unstructured":"Duvall, P., Matyas, S., Glover, A.: Continuous Integration: Improving Software Quality and Reducing Risk, 1st edn. Addison-Wesley Professional, Upper Saddle River (2007)","edition":"1"},{"issue":"1","key":"9720_CR42","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s00355-020-01269-9","volume":"56","author":"A Fabre","year":"2021","unstructured":"Fabre, A.: Tie-breaking the highest median: alternatives to the majority judgment. Soc. Choice Welf. 56(1), 101\u2013124 (2021)","journal-title":"Soc. Choice Welf."},{"key":"9720_CR43","unstructured":"Shadish, W.R., Cook, T.D., Campbell, D.T.: Experimental and Quasi-experimental Designs for Generalized Causal Inference. Houghton, Mifflin and Company (2002)"},{"issue":"2","key":"9720_CR44","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1080\/13876988.2020.1871297","volume":"24","author":"G Capano","year":"2022","unstructured":"Capano, G., Engeli, I.: Using instrument typologies in comparative research: conceptual and methodological trade-offs. J. Comp. Policy Anal. Res. Pract. 24(2), 99\u2013116 (2022). https:\/\/doi.org\/10.1080\/13876988.2020.1871297","journal-title":"J. Comp. Policy Anal. Res. Pract."},{"issue":"2","key":"9720_CR45","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.amepre.2007.04.005","volume":"33","author":"SL Mercer","year":"2007","unstructured":"Mercer, S.L., DeVinney, B.J., Fine, L.J., Green, L.W., Dougherty, D.: Study designs for effectiveness and translation research: identifying trade-offs. Am. J. Prev. Med. 33(2), 139\u2013154 (2007). https:\/\/doi.org\/10.1016\/j.amepre.2007.04.005","journal-title":"Am. J. Prev. Med."},{"key":"9720_CR46","doi-asserted-by":"publisher","unstructured":"Wolff, M., Haase, A.: Viewpoint: dealing with trade-offs in comparative urban studies. Cities 96 (2020). https:\/\/doi.org\/10.1016\/j.cities.2019.102417","DOI":"10.1016\/j.cities.2019.102417"},{"key":"9720_CR47","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2023.107329","volume":"164","author":"R Verdecchia","year":"2023","unstructured":"Verdecchia, R., Engstr\u00f6m, E., Lago, P., Runeson, P., Song, Q.: Threats to validity in software engineering research: a critical reflection. Inf. Softw. Technol. 164, 107329 (2023). https:\/\/doi.org\/10.1016\/j.infsof.2023.107329","journal-title":"Inf. Softw. Technol."},{"issue":"130","key":"9720_CR48","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1002\/ev.364","volume":"2011","author":"CS Reichardt","year":"2011","unstructured":"Reichardt, C.S.: Criticisms of and an alternative to the Shadish, cook, and Campbell validity typology. N. Dir. Eval. 2011(130), 43\u201353 (2011). https:\/\/doi.org\/10.1002\/ev.364","journal-title":"N. Dir. Eval."},{"key":"9720_CR49","doi-asserted-by":"publisher","unstructured":"Robillard, M.P., Arya, D.M., Ernst, N.A., Guo, J.L.C., Lamothe, M., Nassif, M., Novielli, N., Serebrenik, A., Steinmacher, I., Stol, K.-J.: Communicating study design trade-offs in software engineering. ACM Trans. Softw. Eng. Methodol. 33(5), 1\u201310 (2024). https:\/\/doi.org\/10.1145\/3649598","DOI":"10.1145\/3649598"},{"issue":"4","key":"9720_CR50","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1016\/0149-7189(90)90021-N","volume":"13","author":"GD Israel","year":"1990","unstructured":"Israel, G.D., Taylor, C.: Can response order bias evaluations? Eval. Program Plan. 13(4), 365\u2013371 (1990)","journal-title":"Eval. Program Plan."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09720-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09720-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09720-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:53:14Z","timestamp":1742676794000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09720-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,20]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9720"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09720-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,2,20]]},"assertion":[{"value":"28 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 January 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"The authors contacted Inria\u2019s Ethics Review Board (ERB) before survey deployment. The ERB informed the authors that full ERB approval was not required and referred to Inria\u2019s Data Protection Officer for compliance matters. The authors developed a GDPR conformance statement and share only aggregated survey data including open text answers from which information that could identify respondents was removed.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}}],"article-number":"8"}}