Somewhat off-topic, but does anyone know the reason Inria seems to have developed such a specialisation around these types of tools? I get why you'd be there today, but is there a common link/person when that started? If so, I'd love a little nudge about where to find out more.
Edit: Thanks for responses. And a warning to others: don't start following links to advisers and students in Wikipedia, it never finishes.
France has a very mathy culture that emerges from institutions like the Ecole Normale Supérieure, and people like Gérard Huet, Xavier Leroy, Thierry Coquand, etc. who have been among the top scientists in that domain for a while and have aggregated teams around them.
INRIA is an exceptional institution and is able to hire a lot of amazing talent. They were one the earliest public research institutions that had a separate career track for developers and technical staff.
It's truly a national gem. Researchers at INRIA are responsible for scikit-learn, coq, ocaml, etc etc.
It's a national research institutions who's specialized into this sort of thing.
To caricature for US readers, you can think of it as a thousand Google PhD who have a guaranteed job for life and nothing to do but research, any research they might be interested in.
I fear I may have phrased my question poorly. I can understand why you'd gravitate toward there now, I'm more generally curious about how that specialisation came to be in the first place. Was there a specific catalyst? A person or event perhaps.
For example, from my Wikipedia trail I see Maurice Nivat come up in the adviser camp for a few of the more current names.
Out of genuine curiosity, does anyone know how to pronounce the name of this project? I checked the “About Coq” page on the official website, the top-level README in the project’s repository, and the project’s Wikipedia but failed to find any suggested phonetics. There also doesn’t seem to be a definitive answer on the related English Stack Exchange post I found (link: https://english.stackexchange.com/questions/435117/how-is-co...)
Very interesting. So we can derive the phonetics from those provided for coq au vin (/ˌkɒk oʊ ˈvæ̃/), which I have apparently been mispronouncing for a while.
I believe in most North American dialects "corn" is one of the only open "o" in common usage. Try to pronounce an "o" without ending it in a "w" sound. Just holding it longer... and then stop without closing your lips.
Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.
I've never hated a piece of software with the same burning passion I reserve for Coq, but I'm happy to see they are still around releasing new way to brutalize the mind of the unprepared.
Why is that? And what alternative do you prefer? I do not mind it for what it is meant for. I rather would have it more practical (instead of having to write software twice: once to prove it and once to execute it), but that is also very new and experimental, like F* or Idris.
As I said before, it was mostly because it used to crash a lot for weird reasons (I think it didn't really like something in my laptop's memory) and the only explanations I ever got were in French.
If they finally finished translating the documentation and the errors (or fixed whatever memory weirdness was affecting my version) it wouldn't be so bad. I'd still hate it from the countless sleepless night trying to get it start again before the weekly assignment's deadline, though.
I'd be interested in hearing why, or at least hearing the context behind it (i.e. there's a big difference between an undergrad forced to use it for a project and a dependent types researcher who prefers Lean)?
It was about 4 or 5 years ago, when I was in grad school.
The main problem I had with it is that it kept crashing or failing for misterious reason and it just printed out some obscure French error message (which I was forced to pass through Google Translate, since nobody in the whole class could speak French). This only happened for the most obscure errors, while the more common and easy to spot ones (logical errors, typos...) were well documented in English.
Also a lot of useful parts of the manual (and the community posts around it) were written in French.
I don't think it's really inferior to other tools, but the bad documentation and tendency to crash (which I hope had been fixed by now, TBH) got on my nerves.
Lest anyone read this and fear that this is common: In my experience it isn't. Nor was it 4 or 5 years ago. I've never seen Coq crash at all, nor spit out any error message in French, and I was a full-time user for a while.
In my recollection (but I could have read it wrong the first time) it tied to the OS. It had those problem on Linux, but both Mac and Windows users were capable of running it without much hassle (although they did experience the occasional crash). Also, people running Arch had less problems than us running Debian. But I just wanted to pass the course and didn't spend much time debugging it, so it could have been another thing (just a couple of ideas from the top of my head: library versions, conflicts with other running programs, some compiler weirdness...)
Interesting, I've only ever used it on Ubuntu, both with the system Debian packages and with versions built from source (via Opam, the OCaml package manager). Both were rock solid for me. If anything, my understanding is that it's Windows where things are sketchy (for OCaml in general, not Coq specifically). Anyway. I'm sorry to hear you had a bad time. It's probably no consolation that it doesn't seem to be as bad for most others.
> It's probably no consolation that it doesn't seem to be as bad for most others.
I stopped using Coq after that course and moved to other interests, but I'm relatively happy to know that, if I ever need Coq again, the chances for it to be the same PITA I remember are pretty low.
I might not ever need it anymore, but it's a small consolation to know that I don't need to fear that possibility.
Aha, good luck then! I really enjoyed that class, even after things got derailed by Covid. It was like a little problem-solving adventure every week. Still wish there were more Coq in the real world!
I'm from MIT EECS too. Just to clarify for other people - we have a pool of "required courses", from which we only need to choose a few. So it's not like we must learn Coq.
OTOH, I've TAed an undergrad research class and it's mind boggling how many people are doing Coq-related research.
The 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".
Can you say more? My background is in PLT and my half-finished thesis was in Coq - but I've got a real interest in (human) languages too. I'd love to hear about how the two are intermingling.
Working with Coq and trying to understand and use it has been a good brain stretcher for me. It's solidified my understanding of proofs to prove a bunch of simple number theory things in it, as well as creating my own types and experimenting with them.
It's a bit above my academic pay grade, so reading the documentation is always daunting, but I understand the basics. Still can't figure out how to use the notation system.
46 comments
[ 4.1 ms ] story [ 106 ms ] threadEdit: Thanks for responses. And a warning to others: don't start following links to advisers and students in Wikipedia, it never finishes.
It's truly a national gem. Researchers at INRIA are responsible for scikit-learn, coq, ocaml, etc etc.
To caricature for US readers, you can think of it as a thousand Google PhD who have a guaranteed job for life and nothing to do but research, any research they might be interested in.
For example, from my Wikipedia trail I see Maurice Nivat come up in the adviser camp for a few of the more current names.
with French pronunciation on top, English beneath.
Did you really need to name it like that?
Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.
https://coq.inria.fr/V8.1/faq.html#htoc4
If they finally finished translating the documentation and the errors (or fixed whatever memory weirdness was affecting my version) it wouldn't be so bad. I'd still hate it from the countless sleepless night trying to get it start again before the weekly assignment's deadline, though.
The main problem I had with it is that it kept crashing or failing for misterious reason and it just printed out some obscure French error message (which I was forced to pass through Google Translate, since nobody in the whole class could speak French). This only happened for the most obscure errors, while the more common and easy to spot ones (logical errors, typos...) were well documented in English.
Also a lot of useful parts of the manual (and the community posts around it) were written in French.
I don't think it's really inferior to other tools, but the bad documentation and tendency to crash (which I hope had been fixed by now, TBH) got on my nerves.
I stopped using Coq after that course and moved to other interests, but I'm relatively happy to know that, if I ever need Coq again, the chances for it to be the same PITA I remember are pretty low.
I might not ever need it anymore, but it's a small consolation to know that I don't need to fear that possibility.
OTOH, I've TAed an undergrad research class and it's mind boggling how many people are doing Coq-related research.
[1] https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf
It's a bit above my academic pay grade, so reading the documentation is always daunting, but I understand the basics. Still can't figure out how to use the notation system.