Coq Community Survey 2022 Results: Part III
This is the third post summarizing the results of the Coq Community Survey 2022. It covers Coq features, tools, plugins and libraries and their respective popularity. The first part focused on who respondents are, while the second part focused on how they use Coq. . The fourth and last part includes the rest of the results, and the links to the associated research paper and Zenodo artifact.
We invite the Coq community to provide feedback as replies to this post. In particular, we are interested in hearing if something was unclear about survey questions and plots or if you have suggestions for improvements or questions you’d like to see answered with the survey data. For those who prefer, we also welcome feedback in this Zulip topic.
Introduction to the survey
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. The survey was available in English and Chinese, and had 109 questions, some of which were only visible depending on answers to previous questions. See the first post for more detailed information on the survey.
Summary part III: features, tools, and libraries
In this part, the survey working group (WG) looked at responses related to Coq features, Coq-related plugins and tools, and Coq libraries. A basic distinction made in the survey is between core plugins, tools and libraries, most of which are developed and bundled together with Coq, and those from the Coq ecosystem, which are externally developed.
For each item (feature, tool, plugin or library) the survey asked respondents to choose between the options “Advanced user”, “Casual user”, and “Plan to use”, and to skip any item that they did not use nor plan to use. Thus, the plots below present the number of answers in each of these mutually exclusive categories. The survey doesn’t distinguish between respondents who are neither users of nor planning to use an item, and those who skipped answering the question (e.g., because they ran out of time or patience). The WG chose this approach to reduce the time needed to complete the survey. In each plot, the items are ordered by their number of reported users.
For each item, the survey also asked respondents to choose between “Impossible to do without” and “Hard to do without”, which we call the criticality of the item. The survey does not distinguish between features that can be done without and those that respondents skipped for other reasons. Note that the item order in a plot for criticality may differ from the corresponding plot for usage.
Language features
Coq’s language features are either part of the core language or are considered extensions of the core. For example, the core includes inductive types and the more recent SProp sort of proof-irrelevant propositions, while extensions include typeclasses and canonical structures. As demonstrated by the UniMath library, even basic features such as inductive types, which many respondents consider indispensible, can be considered optional.
Tactics and tactic languages
Coq provides many built-in proof tactics, which we call the standard tactics. A few of these tactics are implemented in Coq’s oldest dedicated tactic language, Ltac, which is also available to users to create custom tactics. Other tactic languages are available, either bundled with Coq itself (Ltac2) or available via the Coq ecosystem (Mtac2, MetaCoq, and Coq-Elpi). SSReflect is a set of tactics that provide an alternative to the standard tactics.
Extraction
Coq supports extraction of functions and data to several functional programming languages, which removes computationally irrelevant information while preserving behavior. For example, the build process of the CompCert compiler project performs extraction of verified Coq functions to OCaml.
In addition to usage of existing extraction targets, we asked what other extraction targets respondents would like to have. The responses were diverse, with Rust and C the most popular choices. Targets not currently supported by Coq may still be supported by packages in the Coq ecosystem. For example, Rust extraction is available in the ConCert framework.
Other features
We included questions on a final set of Coq features that are useful in some contexts and can be enabled inside Coq or passed as options to the Coq batch compiler. For example, the vos/vok compiled interfaces allow faster batch compilation by skipping (some) proof checking, and the par goal selector can speed up tactic proofs by parallelization.
A key motivation for asking about usage of some of these features was to determine the impact of their potential removal. For instance, the Add LoadPath feature is being deprecated in Coq 8.16. If you are among the 18 users for which this feature is important, the Coq developers recommend that you open an issue to let them know of your use case.
Core plugins and tools
Plugins are optional extensions to Coq that provide additional tactics or functionality. Core plugins are the ones bundled with Coq, plus Bignums and Equations. Bignums was previously bundled. Equations was primarily developed by a Coq core team member and is a possible alternative to the Functions plugin. Core tools are external programs bundled with Coq, which include the Coqdoc documentation generator and the coq_makefile tool for producing makefiles to build a Coq project.
Standard library
Coq’s standard library (Stdlib) is a collection of Coq theories bundled with Coq. Stdlib contains basic datatype definitions and logical definitions (the prelude loaded by default when starting Coq), along with formalizations of numbers (e.g., Arith and ZArith) and other more advanced structures (e.g., Sets and Vectors). Unlike ecosystem libraries, which may be usable with multiple releases of Coq, Stdlib is specific to each Coq release.
Ecosystem plugins and tools
In contrast to tools like Coqdoc, external plugins and tools such as CompCert are not maintained as part of the Coq GitHub repository, but separately by members of the more loosely organized Coq ecosystem. However, some ecosystem projects include Coq core team members as maintainers, and a large majority of the projects listed here are part of the Coq Platform.
Note that plots after this point use a different X-axis scale than plots before this point (up to 160 respondents, whereas the ones before this point had up to 500 respondents). These scales are arbitrary and were chosen to make the plots more readable, since the ecosystem tools and libraries have fewer users than the core tools and libraries.
Ecosystem libraries
We divide ecosystem libraries into general libraries, domain-specific libraries and Mathematical Components libraries. General libraries provide basic datatypes, functions and results likely to be useful regardless of the Coq application domain. They either complement Stdlib (Coq-ExtLib, Coq-std++, and Math Classes) or provide alternatives to it (Mathematical Components and TLC).
Domain-specific libraries provide definitions and results related to a mathematical foundation or area (e.g., UniMath, HoTT, and CoRN), or provide support for specific applications such as programming language semantics and program verification (e.g., Iris and VST).
The Mathematical Components library consists of several core sublibraries (ssreflect, fingroup, algebra, solvable, field, character), as can be seen in the latest library graph. In addition, there are external libraries, e.g., multinomials and analysis, that depend on (some of) the core sublibraries.
