Zulip Chat Archive

Stream: general

Topic: Coq community survey 2022

Eric Wieser (Jan 30 2022 at 21:18):

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

Notification Bot (Jan 30 2022 at 21:25):

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

Mario Carneiro (Jan 30 2022 at 21:26):

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 (Jan 30 2022 at 21:26):

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

Patrick Massot (Jan 30 2022 at 21:27):

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

Patrick Massot (Jan 30 2022 at 21:28):

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 (Jan 30 2022 at 22:05):

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 (Jan 31 2022 at 03:09):

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 (Jan 31 2022 at 09:02):

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 (Jul 25 2022 at 19:54):

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 (Jul 26 2022 at 12:29):

Very interesting, thanks for sharing!

Karl Palmskog (Aug 03 2022 at 16:30):

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 (Aug 03 2022 at 19:13):

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

Filippo A. E. Nuccio (Aug 03 2022 at 19:23):

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

Karl Palmskog (Aug 04 2022 at 18:16):

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 (Aug 04 2022 at 20:47):

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 (Aug 04 2022 at 21:29):

@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 (Aug 04 2022 at 21:54):

@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 (Aug 04 2022 at 21:57):

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 (Aug 04 2022 at 21:59):

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 (Aug 05 2022 at 09:05):

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 (Aug 05 2022 at 10:32):

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 (Aug 05 2022 at 10:48):

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 (Aug 13 2022 at 14:22):

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 (Aug 13 2022 at 14:51):

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 (Aug 13 2022 at 14:57):

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 (Aug 13 2022 at 15:00):

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 (Aug 13 2022 at 15:50):

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 (Aug 13 2022 at 17:48):

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

Karl Palmskog (Aug 13 2022 at 17:59):

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 (Aug 13 2022 at 18:01):

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 (Aug 31 2022 at 11:43):

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 (Aug 31 2022 at 12:20):

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 (Aug 31 2022 at 13:00):

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 (Aug 31 2022 at 20:27):

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

Karl Palmskog (Aug 31 2022 at 21:25):

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

Last updated: Aug 03 2023 at 10:10 UTC