Coq community survey 2022

Stream: general

[Eric Wieser]

Ah. That question doesn't appear if you answer "I have never used Coq"

[Notification Bot]

This topic was moved here from #announce > Coq community survey 2022 by Mario Carneiro

[Mario Carneiro]

Indeed, the survey seems to lack a place for people who have not used Coq because of some barrier or another and want to explain why

[Patrick Massot]

Karl's message was pretty explicit: "Dear Lean community members who have used or are using Coq,"

[Patrick Massot]

I think it's reasonable that they created a survey specifically for person who have been using Coq.

[Patrick Massot]

I've tried Coq for a couple of weeks before switching to Lean but I wouldn't feel legitimate to answer this survey. I didn't try hard enough.

[Arthur Paulino]

There might be still valuable feedback as to why you've switched to Lean (as so did I).
They also ask about feedback on a name change, and I was eager to support that :upside_down:

[Karl Palmskog]

we consciously constructed the survey so that it can be responded to even if someone doesn't use Coq (although with many fewer questions, and hiding questions about "other proof assistants"). But here I was indeed trying to reach people who tried Coq in the past and switched to Lean, or are using Coq in parallel with Lean. Those Coq+Lean users can be explicitly tracked in the survey data, and aggregate information about them may be of interest to the Lean community.

[Karl Palmskog]

in my view, someone that only tried Coq for as little as a few weeks would still be eligible to answer, though. There is no requirement to "try hard" to use Coq to count as a Coq user to us.

[Karl Palmskog]

We released in the initial part of the Coq community survey 2022 result summary. The Lean community may be intererested in the following results: https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730/1#experience-with-other-proof-assistants-24 (https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/other-proof-assistants-barplot.png)

We can also see that the Coq community tilts toward traditional CS application domains, which may be a difference between the Lean and Coq communities: https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730/1#coq-application-domains-22 (https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/coq-application-domains-barplot.png)

[Filippo A. E. Nuccio]

Very interesting, thanks for sharing!

[Karl Palmskog]

We posted the second part of the Coq community survey result summary: https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746

In comparison to Lean, many Coq users are seemingly more keen on Emacs (& ProofGeneral) as an IDE over VS Code (https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ide-multiple-barplot.png)

[Patrick Massot]

Is there something like Lean widgets in Coq? Otherwise the editor question is completely different.

[Filippo A. E. Nuccio]

There is a reasonably nice VSCode extension for Coq (VSCoq); no widgets, though.

[Karl Palmskog]

this graph is from the first part, but may be worth flagging up here if someone missed it, as it may also illustrate community differences: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/research-topics-barplot.png

TLDR: most popular areas [multiple choice] are: programming languages, formal methods, logic. Math topics like algebra, analysis, topology come in at 11% or less of respondents each

[Kevin Buzzard]

I think this is one of the most telling observations! Did you ask any questions of the form "are you a constructivist"? I suspect that you might get very different answers again in the Lean/Coq communities. I've told this story many times before, but in 2017 I was genuinely of the opinion that constructivism had died out; I had no idea it was alive and well in CS departments; that's how seriously the concept was being taken in all the maths departments I've worked at.

[Jason Rute]

@Kevin Buzzard I think many modern “constructivists” aren’t holding a die-hard philosophical position on what basic facts of math are true, but are just intellectually interested in constructive mathematics in the same way you are in algebraic geometry and set theorists are interested in set theory. (Constructive math has a lot of applications to classical mathematics and computer science.) so I don’t know the term “constructivist” is that useful anymore. The question should just be “do you research (or are you interested in) constructive mathematics”?

[Karl Palmskog]

@Kevin Buzzard we didn't ask anything about constructivism (or philosophy of math in general), but we can keep this in mind for the next survey.

@Jason Rute that's a good formulation, thanks, I will pass this on to our working group.

[Kevin Buzzard]

I only mention it because I still regard it as a really stark difference between what people study in maths departments and what they study in CS departments.

[Karl Palmskog]

I'm not a bonafide constructivist or intuitionist, but what is nice about constructivism is that I don't need a different language to describe computability, which can be important in many CS applications. Larry Paulson mentioned the "synthetic" approach to computability theory that this has spawned as a nice application of constructive type theories in his blog post here: https://lawrencecpaulson.github.io/2022/04/20/Why-constructive.html

[Patrick Massot]

In principle I very much agree with Jason's comment. But one should keep in mind the practical effect for formalization. We've seen with mathcomp and mathlib that it is very hard to make a library which is both classical and constructive. Hence even if you don't have a "die-hard philosophical position", the effect is the same: it seems any big library has to strongly impose one side.

[Karl Palmskog]

if anyone caught the recent presentation by Gonthier, he mentions mostly practical concerns (rather than philosophical aims) in creating MathComp. So the axiom-freedom of the core MathComp libraries may be mostly due to minimalism and design concerns (axioms don't compose well in Coq, library developers adding one axiom constrains what axioms library users can add)

[Jason Rute]

I agree with Patrick that in a given project one has to make a choice if one is going to be careful or carefree about axioms, and maybe that could be another question on the survey. (Also with the recent interest in univalent mathematics, it gets subtle since one could be “carefree”, but in the sense one does freely uses univalence and HITs, although I’ve yet to see a library freely using univalence, HITs, LEM, and AC.)

[Karl Palmskog]

Some presentation slides with additional survey results became public, including some plots on the renaming question: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/coq-workshop-2022.pdf

(The "new" plots will appear in blogposts in due time, along with additional plots)

[Kevin Buzzard]

The slides seem to imply that there was a survey in 2014. Did some of the questions coincide and, if so, were there any interesting changes between 2014 answers and 2022 answers?

[Karl Palmskog]

slides for 2014 survey here: https://github.com/braibant/coq-survey/blob/master/popl-coq.pdf

Some obvious things:

• we have significant share of people from industry now
• VS Code shows up and becomes popular
• relatively more Mac users back then, Linux more popular now
• tactic language explosion, SSRreflect gets many users
• Lean shows up, otherwise similar "other proof assistants" experience

[Karl Palmskog]

we took inspiration from the 2014 survey, and some questions partially carried over, but I don't think we kept any question exactly the same

[Karl Palmskog]

Mostly speculation, but I think Linux share can be used as a proxy variable of sorts for share of "CS-oriented users". My impression is that the more math-y you are [as opposed to CS-y], the higher the chance of being macOS user.

[Kevin Buzzard]

The vast majority of my UG Lean users are on Windows BTW!

[Karl Palmskog]

ah, this would be consistent with our data on newcomers (relatively more Windows): https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/os-multiple-barplot.png

[Karl Palmskog]

so maybe a stereotypical proof assistant user starts as a Windows user at UG level, then branches into macOS or Linux, depending on disposition (and there is likely a large number that just stop using proof assistants and continue to use Windows)

[Karl Palmskog]

we posted the third part of the Coq community survey results, which looks at usage of Coq features, tools, plugins, libraries: https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777

For Lean 4 implementers, maybe the following graph could be relevant to what future features to consider: https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/features-barplot-stacked.png

[Alex J. Best]

I'd find it interesting to see some graphs on how some of these answers correlate, e.g are people using different extensions of the standard library only using one, or mixing multiple? Or how do different research interests correlate with choice of tactic language used. Is such data available and would it be possible to include in upcoming posts?

[Karl Palmskog]

we have the raw data to study such connections, yes (but not at a deep level, only based on people selecting multiple libraries, tactics, etc.). There may be additional blog posts where we show "intersections" like that, I'll pass on the idea

[Jason Rute]

I’m still understanding Coq modules (the second most popular feature.). When are they used and what are the Lean alternatives?

[Karl Palmskog]

modules are (arguably) mostly used for hiding contextually-irrelevant definitions and results. I believe Lean has some namespacing feature that does something similar? The Coq module system is like modules in languages like OCaml and Standard ML