[TYPES/announce] Summary of results from the Coq Community Survey 2022

[Théo Zimmermann]

Dear TYPES/announce subscribers,

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.

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.

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.

Post 1: Who is using Coq and in what context? (
https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDATsDnRuM$  )

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.

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.

Post 2: How people are using Coq (
https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDAN4xD4HM$  
)

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.

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.

Post 3: Usage of Coq features, tools, and libraries (
https://urldefense.com/v3/__https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777__;!!IBzWLUs!S0edeJeC_2Oe_NYHa0nZu4zhCu32CkpWG5kLqd3VkuJqGM6y82PA3kJNA6z7if9OJueOdSkB8am3Ws2udjDAjcfnjao$  
)

This post examines responses related to Coq features, Coq-related plugins
and tools, and Coq libraries, in particular their respective popularity and
criticality.

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.

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.

Théo Zimmermann, for the Coq Community Survey 2022 working group
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220922/ded6b4d1/attachment.htm>