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.
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
there is a Universities teaching Coq wiki page also.
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
I used the excellent lecture notes from Saarland university to learn the basics.
regarding the Saarland course(s), there is a book nowadays: https://github.com/uds-psl/MPCTT
I'm teaching first year masters students from Software Foundations book 1, 2 and QC, with added chapters for Equations and Monads.
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.
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.
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...
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.
(I vaguely understand INRIA's mission is somewhat different)
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.
and one might get some credit for experience with systems like Coq in grant applications, and for open source projects
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.
(this is why the "authors" and "copyright owners" are often distinct, and is what will kill most relicensing efforts of Coq-related projects)
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.
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