Stream: Miscellaneous

Topic: Universities teaching Coq


view this post on Zulip Huỳnh Trần Khanh (Jan 15 2023 at 04:25):

Are there actual universities that teach Coq, or do you just find out about Coq on your own, word of mouth, a genuine desire to write bug free programs, etc? Judging by the activity here, looks like self taught folks are the majority... And by "teach" I mean a real course and not I can go to room X and there'd be folks well versed in Coq.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 05:45):

We asked questions in this direction in the survey. According to the results, many people actually hear about Coq in a class, and then learn Coq through classes or as part of academic work. The typical application domains are indeed in software verification, but general PL research and formalization of math are also common.

hear about plot, learn plot, applications plot

view this post on Zulip Karl Palmskog (Jan 15 2023 at 05:48):

there is a Universities teaching Coq wiki page also.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 06:16):

I think it's also common for PhD students to do ad-hoc reading classes on a topic that are then credited as regular courses, even if it's not a "real course" but rather 2-5 people having regular seminars. I learned Coq this way as a PhD student by following the Coq'Art book

view this post on Zulip Stefan Haan (Jan 15 2023 at 12:26):

I used the excellent lecture notes from Saarland university to learn the basics.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 13:02):

regarding the Saarland course(s), there is a book nowadays: https://github.com/uds-psl/MPCTT

view this post on Zulip Bas Spitters (Jan 15 2023 at 15:48):

I'm teaching first year masters students from Software Foundations book 1, 2 and QC, with added chapters for Equations and Monads.

view this post on Zulip Huỳnh Trần Khanh (Jan 15 2023 at 15:57):

Man. And btw who are in charge of the Coq open source projects? Especially the fun stuff like jsCoq, SerAPI and coq-lsp. Unpaid enthusiasts? I wouldn't be surprised if the work is unpaid, but it's kinda disheartening as a lot of time and effort is put into the projects.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:01):

again according to the survey, a majority of people using Coq have academic employment, and there are many (graduate) students (plot). A reasonable assumptions is that this is representative of people running open source Coq projects. There was also a paper last year on the Coq ecosystem which emphasizes the research side.

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 16:02):

To expand on that: researchers have salaries, and _tenured_ researchers have stable employment and varying amount of academic freedom, but the job description emphasizes publishing papers, not writing software, especially not software that's as usable as Coq...

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:03):

so people are in some sense, and to some extent, getting paid to work on Coq-related projects. Compare Linux and its ecosystem, where to my knowledge the most profilic contributors are employed by companies with Linux-related business.

view this post on Zulip Paolo Giarrusso (Jan 15 2023 at 16:03):

(I vaguely understand INRIA's mission is somewhat different)

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:07):

the tenure systems are quite different across countries. There is generally no guarantee across Europe to get to work on/with Coq (if that's what you like), just because you have a permanent academic position. But people might find ways to shoehorn it in, if that's their comparative advantage.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:08):

and one might get some credit for experience with systems like Coq in grant applications, and for open source projects

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:18):

I don't have much industry working experience, but I imagine it might be (more) difficult to do Coq-related open source there. I had some colleagues who had to negotiate quite hard to get written permission (non-Coq-related). In most countries, the employer owns all your code by default (even written on spare time), and will forbid any sublicensing.

view this post on Zulip Karl Palmskog (Jan 15 2023 at 16:20):

(this is why the "authors" and "copyright owners" are often distinct, and is what will kill most relicensing efforts of Coq-related projects)

view this post on Zulip Pierre Jouvelot (Jan 15 2023 at 17:25):

Huỳnh Trần Khanh said:

Man. And btw who are in charge of the Coq open source projects? Especially the fun stuff like jsCoq, SerAPI and coq-lsp. Unpaid enthusiasts? I wouldn't be surprised if the work is unpaid, but it's kinda disheartening as a lot of time and effort is put into the projects.

The jsCoq project and its related components are developed by @Emilio Jesús Gallego Arias and a few other participants. Emilio is currently employed by Inria.

view this post on Zulip Théo Zimmermann (Jan 16 2023 at 10:24):

Emilio is currently employed by Inria.

As a researcher, so he also needs to prove his worth by writing papers...


Last updated: Oct 13 2024 at 01:02 UTC