[HN Gopher] Coq 8.13
___________________________________________________________________
Coq 8.13
Author : infruset
Score : 108 points
Date : 2021-02-18 14:23 UTC (8 hours ago)
(HTM) web link (coq.inria.fr)
(TXT) w3m dump (coq.inria.fr)
| [deleted]
| threatofrain wrote:
| What is the industry or academic prevalence or level of optimism
| for Coq / Lean?
| raptortech wrote:
| Sample size of 1: I'm an EECS PhD student at MIT and one of my
| required courses (6.822) is taught entirely in Coq
| mncharity wrote:
| 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".
|
| [1] https://frap.csail.mit.edu/main [2]
| http://adam.chlipala.net/frap/frap_book.pdf
| mcncm wrote:
| Any chance you took FRAP last spring? Hi, maybe-classmate :)
| tracyhenry wrote:
| 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.
| sinkasapa wrote:
| Theorem provers are increasingly popular in certain areas of
| linguistics.
| wk_end wrote:
| 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.
| iandinwoodie wrote:
| 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...)
| tom_mellior wrote:
| The general answer to "how to pronounce word X in language Y"
| is https://forvo.com/. In this case:
| https://forvo.com/word/coq/#fr
| bigdict wrote:
| It's pronounced cock, coq means rooster/cock in French.
| fovc wrote:
| The o sound is slightly different. More like the first o in
| bottom
| ta8645 wrote:
| That sounds the same to my ear. At least the way I
| pronounce both words. c-awe-ck and b-awe-ttom.
| Pet_Ant wrote:
| 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.
| Erlangen wrote:
| You can listen here for the difference,
| https://www.linguee.fr/francais-
| anglais/search?source=auto&q....
|
| with French pronunciation on top, English beneath.
| iandinwoodie wrote:
| Very interesting. So we can derive the phonetics from those
| provided for coq au vin (/,kak oU 'vae/), which I have
| apparently been mispronouncing for a while.
| bnegreve wrote:
| From coq FAQ:
|
| 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
| noblethrasher wrote:
| Also, Thierry Coquand, who is behind CoC, and is also one of
| the developers of the software that became Coq.
| frollo wrote:
| 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.
| tluyben2 wrote:
| 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.
| frollo wrote:
| 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.
| tobmlt wrote:
| This is a beautiful, dark humored, hilarious comment. Thanks
| for it!
| [deleted]
| bidirectional wrote:
| 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)?
| frollo wrote:
| 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.
| julienreszka wrote:
| Liar
| tom_mellior wrote:
| 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.
| deathtrader666 wrote:
| Alright, but why?
| Tyr42 wrote:
| I used it, and while I didn't hate it, I can totally see why
| it could inspire someone to write such a comment.
| bigdict wrote:
| For Harambe?
| [deleted]
| JNRowe wrote:
| 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.
| davidivadavid wrote:
| France has a very mathy culture that emerges from institutions
| like the Ecole Normale Superieure, and people like Gerard 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.
| alentist wrote:
| Jean-Yves Girard is another one.
| Fede_V wrote:
| 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.
| user5994461 wrote:
| 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.
| JNRowe wrote:
| 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.
| apetersonBFI wrote:
| 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.
| iso8859-1 wrote:
| The release notes do not spell Xia Li-yao consistently. Which is
| family name, and which is given?
___________________________________________________________________
(page generated 2021-02-18 23:02 UTC)