<div dir="ltr">Dear TYPES/announce subscribers,<br><br>The Coq Community Survey 2022 was an online public survey conducted during February 2022, previously announced on this mailing list. The survey working group (WG) is happy to announce that a summary of results from the survey is now available.<br><br>The main goal of the survey was to get an updated picture of the Coq user community and inform future decisions made by the Coq team and other Coq ecosystem participants. The survey was advertised to Coq users primarily via the Coq Discourse forum, the Coq Zulip chat, Coq-club mailing list, Coq Twitter, and the Coq website, as well as related mailing lists such as this one. On behalf of the survey WG, I would like to thank everyone in the type theory community that participated by responding to the survey.<br><br>The survey was available in English and Chinese, and had 109 questions, some of which were only visible depending on answers to previous questions. Answering was optional for all survey questions, and most questions allowed free-text answers. The survey received 466 responses, and the WG has now collaboratively produced three posts that summarize these responses.<br><br>Post 1: Who is using Coq and in what context? (<a href="https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDATsDnRuM$">https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730</a>)<br><br>This post examines the demographics of the Coq users who took the survey, and in what context they are using Coq. “Context” here means users’ experience before they started to use Coq, their reasons for using Coq, and their experience with related languages and tools.<br><br>The demographic responses suggest that the Coq community is tilted toward computer science, not least in educational background and application areas. France and the United States are where half of the respondents are located, but we observed more diversity in the locations of newcomers.<br><br>Post 2: How people are using Coq (<a href="https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDAN4xD4HM$">https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746</a>)<br><br>This post examines how respondents use Coq on a daily (or weekly or yearly) basis. This includes the Coq version and IDE, and software infrastructure such as operating system and package management.<br><br>The responses suggest that most Coq users run Linux-based systems and directly use the opam package manager. Emacs (with ProofGeneral) remains the most popular Coq code editor, but is closely followed by CoqIDE and VS Code.<br><br>Post 3: Usage of Coq features, tools, and libraries (<a href="https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDAjcfnjao$">https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777</a>)<br><br>This post examines responses related to Coq features, Coq-related plugins and tools, and Coq libraries, in particular their respective popularity and criticality.<br><br>The responses suggest that Coq’s typeclasses are relatively popular (trailing inductive types and modules as a language feature), that the Dune build system is gaining users, and that Mathematical Components is the most popular general library besides Coq’s standard library. In addition, proof automation tools such as CoqHammer and SMTCoq, and modern tactic languages such as Ltac2, currently have few users, but many prospective users.<br><br>The WG welcomes feedback from the type theory community as replies in each Discourse forum post. In particular, we welcome suggestions for improvements or questions that could be answered with the survey data. Other Discourse forum posts as well as more formal publications may follow to complete the analysis of the results.<br><br>Théo Zimmermann, for the Coq Community Survey 2022 working group</div>