Where are the Coq communities and enthusiasts?

kytrinyx commented 6 years ago

As we move towards the launch of the new version of Exercism we are going to be ramping up on actively recruiting people to help provide feedback.

Our goal is to get to 100%: everyone who submits a solution and wants feedback should get feedback. Good feedback. You can read more about this aspect of the new site here: http://mentoring.exercism.io/

To do this, we're going to need a lot more information about where we can find language enthusiasts.

Is Coq supported by one or more large organizations?
Does Coq have an official community manager?
Do you know of specific communities (online or offline) that are enthusiastic about Coq? (Chat communities, forums, meetups, student clubs, etc)
Are there popular conferences for Coq? (If so, what are some examples?)
Are there any organizations who are targeted specifically at getting certain subgroups or demographics interested in Coq? (e.g. kids, teenagers, career changers, people belonging to various groups that are typically underrepresented in tech?)
Are there specific groups or programs dedicated to mentoring people in Coq?
Are there popular newsletters for Coq?
Is Coq taught at programming bootcamps? (If so, what are some examples?)
Is Coq taught at universities? (If so, what are some examples?)

In other words: where do people care a lot and/or know a lot about Coq?

This is part of the project being tracked in https://github.com/exercism/meta/issues/103

Bubbler-4 commented 5 years ago

Large organizations

Coq was originally developed at INRIA, and it is currently supported by Inria Foundation. Microsoft Research-Inria Joint Center is using Coq for formal methods research projects, one of which is MathComp.

Coq communities

Some of the communities are listed here.

Conferences

ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
- Co-hosting CoqPL workshop
Interactive Theorem Proving (ITP)
- Co-hosting Coq workshop

Programming bootcamps(?)

Some are listed at the bottom of this page. I doubt I can call them bootcamps, but there are some summer/winter schools on Coq targeted for mostly graduate students.

University courses

Some universities teach Coq using Software Foundations (SF), CPDT and/or FRAP. Usually SF is the primary text because it has the slowest learning curve and lots of exercises. Many such courses are offered at graduate level.

kytrinyx commented 5 years ago

Thank you @Bubbler-4 !

This is a really great collection of resources. I'm going to go ahead and close this, and if we need to dig further later we can either reopen it or open a new issue with specific questions.

exercism / coq