The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

We did our entire graduate PL course in Coq at University of Washington this year. This includes grad students outside of PL/verification. Haven't seen a lot of it in undergrad in the US, but I got a brief intro at Maryland in 2012.

I think the real question is how people define "capable" when they cite those numbers. Are we talking about people who can use Coq to verify large systems or people can verify small languages for the sake of class projects? The latter is probably much larger than the former.

On Jan 22, 2016 7:34 AM, "Soegtrop, Michael" <michael.soegtrop AT intel.com> wrote:

Dear John,

> At work I keep hearing the figure "1,000" as an approximation of the number
> of capable Coq programmers in the world. What would a closer number be
> now in 2016?

I have heard 100 ;-) so I found this rank 70 quite astonishing. Form what I hear more and more universities offer lectures in Coq and a good fraction of computer science students are taking these lectures. Maybe a large part of the Coq question on stack exchange comes from students doing exercises - I don't know. It might take a few more years until the students taking Coq lectures now hit the industry, but it will happen.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928