Do we make an effort to be a serious research forum? The Lean Zulip goes to great lengths to be a serious research forum, and that makes me mildly uncomfortable. Not least because I am just an enthusiast :pensive: Honestly I'm just learning this stuff because I think formal verification and competitive programming go well together.

My current impression is this place is more relaxed, and I don't have to do research to fit in. And I see that there are fellow enthusiasts here as well. It's less active than the Lean Zulip but that's ok, if I ask a question I still get an answer reasonably quickly.

This topic was moved here from #Coq users > Serious research forum by Karl Palmskog.

since this is a more general question, I'll move it to the Misc stream. In contrast to Lean, which focuses 100% on the Zulip, Coq has many forums, such as the Coq-Club mailing list, Discourse Forum, etc., see https://github.com/coq-community/awesome-coq#community

you can see here that the Coq community is diverse in research backgrounds and topics and goals, so it's unlikely that the Zulip will be a particular focus for research over time. Some of us use it for research projects related to Coq, though

we don't really have a pipeline like Lean for learning the proof assistant and contributing to a specific library. The closest may be the Coq-community contributing guide: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md#contributing-guide

... and maintainer-wanted tag for Coq-community projects: https://github.com/coq-community/manifesto/issues?q=is%3Aissue+is%3Aopen+label%3Amaintainer-wanted

@Huỳnh Trần Khanh have you seen Andrew Appel's Coq ecosystem paper? It looks at Coq mostly from a program verification angle: https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf

Last updated: Jun 10 2023 at 06:31 UTC