In this post, we give an introduction to the survey and then provide the first part (out of three planned parts) of a result summary. This part is about who is using Coq and in what context. See also the second part on how people are using Coq.
We invite the Coq community to provide feedback on our summary as replies to this forum post. In particular, we are interested in hearing if something was unclear about survey questions and plots.
The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to obtain an updated picture of the Coq user community and inform future decisions taken by the Coq team and other Coq ecosystem participants. In particular, the survey aimed to enable effective decision making about the development of the Coq software, and also about matters pertaining to Coq ecosystem software maintained by users in academia and industry.
The survey was designed, deployed, managed, and analyzed by members of a working group (WG), which was formed following a public call for participation by the Coq core team.
Survey questions were created by WG members collaboratively. The WG took inspiration from the previous Coq Community Survey in 2014, and similar more recent surveys for OCaml and other programming languages. Efforts were made to adhere to survey best practices, e.g., on ordering demographic questions late to avoid their answers affecting other questions.
The deployed survey was advertised to Coq users primarily via the following Coq community forums: Discourse, Zulip chat, Coq-club mailing list, Coq Twitter, and the Coq website. The WG also advertised in more general venues and other related communities, e.g., the Types-announce mailing list, Agda and Lean Zulip chats, and on language-specific forums in Chinese and in French (mailing lists of GDR IM and GPL).
After the survey closed, WG members collaboratively analyzed the response data, primarily using Jupyter. For GDPR conformance, the raw survey data was kept within the EU, using only Inria-hosted tools.
The survey - available in English and Chinese - has 109 questions, some of which were only visible depending on answers to previous questions. Broadly, the survey asked about (i) use of Coq features, IDEs, libraries, plugins, and tools, (ii) views on renaming Coq, on Coq improvements, and issues such as inclusion, and (iii) demographic data, such as age, gender, and experience with Coq and other proof assistants or programming languages. Answering was optional for all survey questions, and most questions allowed free-text answers. In particular, it was possible to answer the survey without having used Coq, albeit with many questions hidden.
In this summary part, the WG looked at 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 similar languages and tools.
WG members expected, based on interactions in the various Coq community forums, the two top locations of respondents to be France (which is where Coq was initially created and where most of its core developers are still located) and the United States. However, some were surprised by the relatively high number of respondents from the United Kingdom, which already hosts separate communities around other proof assistants based on the HOL logic and Lean.
The number of respondents from China mainland was likely boosted by the availability of a Chinese version of the survey. 44 respondents used the Chinese version, including the 30 respondents from China mainland, but also several outside China mainland, along with some who did not provide their location.
We provide a separate bar chart with the full list of locations of respondents, i.e., not just the top seven.
Coq is a demanding tool to learn, and people are primarily exposed to it during (university) classes. Hence, it is in line with the WG’s expectations that the majority of users are in the 20-39 age range. Having many young respondents (20-29) may be a result of community growth in that age group.
Based on the WG’s observations of Coq community channels such as the Zulip chat, the Coq-club mailing list, and participation at academic conferences such as POPL, the expectation was that the majority of respondents would be academic researchers and students. However, we observe that the private sector represents a quite significant share as well.
Historically, Coq has been used mainly by researchers and graduate students, which is reflected in a high number of respondents with PhD degrees. In many universities, courses that use or teach Coq are considered advanced, and may thus not be available to undergraduate students (with high school or equivalent as highest obtained education).
By combining the responses on education and employment, it is possible to categorize respondents into “undergraduate students” (students with a high school diploma), “graduate students” (students with bachelor’s or master’s degrees) and “PhD academics” (respondents employed in academia who have a PhD degree). Note that the percentages are relative to the total number of respondents that fit in one of these three categories.
Most respondents have experience with all the three major programming styles. Logic programming (which can be emulated in Coq using inductive predicates and other techniques and tools) is a minority style, but still prevalent among respondents.
OCaml was developed in part as the implementation language of Coq, is primarily developed in France, and is taught to French undergraduate students in several French universities. Consequently, the WG expected many respondents would have experience with OCaml. However, Haskell experience turned out to be more prevalent among respondents. Nevertheless, many respondents have experience with both Haskell and OCaml, along with other languages such as Scheme.
The follow-up second question below was only shown to people who answered that Coq was well-established in their workplace.
Agda is the most-used other proof assistant among respondents. This may be due to several factors, such as (i) shared heritage with Coq, (ii) shared foundations with Coq, and (iii) Agda community forum outreach for the survey.