Functional Programming in Coq | Hacker News Reader

Functional Programming in Coq

softwarefoundations.cis.upenn.edu

65 pointsatan230 comments

Open articleView on HN

Volume 2: Programming Language Foundations

https://softwarefoundations.cis.upenn.edu/plf-current/index....

Volume 3: Verified Functional Algorithms

https://softwarefoundations.cis.upenn.edu/vfa-current/index....

Volume 4: QuickChick: Property-Based Testing in Coq

https://softwarefoundations.cis.upenn.edu/qc-current/index.h...

Volume 5: Verifiable C

https://softwarefoundations.cis.upenn.edu/vc-current/index.h...

Volume 6: Separation Logic Foundations

https://softwarefoundations.cis.upenn.edu/slf-current/index....

OK so the name is funny and that's a whole subthread already.

Does anyone here use coq to build stuff? What stuff, and crucially for me, why did you pick it over isabelle or lean? Or acl2, or others

I want to start using theroem provers in compiler construction and getting going is a bit like trying to get sane guidance on what programming language to learn first.

CompCert is a good example of Coq used to develop complex commercial proven correct software.

What ever happened to the effort [1] to rename Coq in order to make it less offensive? There were a number of excellent proposals [2] that seemed to die on the vine.

[1] https://github.com/coq/coq/wiki/Alternative-names

[2] https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3...

What kind of person is offended at this? It's not even in the ballpark of making the allusion (let alone whether someone should be offended at such an allusion). I refuse to believe there are people this petty.

> I refuse to believe there are people this petty.

There's a lot of us who aren't petty, but uhhh, certainly childish. The name is a problem.

It's a problem for those people, and the solution is to grow up.

Why should adults care?

Because nobody wants to say they program in cock

1- Languages other than English exist, deal with it

2- Grow up

3- Say "cee-oh-queue"

> Say "cee-oh-queue"

This is the correct answer if you are truly unable to say "Coq".

If you need a precedent for multiple ways to refer to the same language, SQL has your back.

In French, the way the word "bit" is pronounced sounds the exact same as the French word for cock (not the rooster).

I can assure you that French CS programming students get over it quickly. There's noone really asking for it to be renamed because it's understood that it's a commonly used foreign word. I'm not sure why an English professional scientist or programmer would be unable to take the same stance for a programming language invented in another country.

i don't get it - are you (or they) childish and therefore giggling to yourself (themselves)? okay? i still don't see who is offended?

Try saying the word "pussy" repeatedly in a business or technical conversation.

you're assuming that everyone lives in the same shoes as you do - i curse in a professional context very regularly (fuck, shit, etc). i have given technical presentations (that are recorded and made public - youtube) at decently sized venues in the same tone.

People like you are a problem.

Reporting for duty!

Coq means rooster in French and is not used as an insult or an euphemism for the penis at all. It's also what's on the logo.

Cock also means rooster in English, so really one might say it's perfect in both English and French.

Interestingly, coq is from Latin coccus (rooster) and cock is from Germanic kukkaz (rooster). I don't think there are many words that exist in both French and English with nearly identical pronunciation, the same meaning but unrelated roots!

I wonder of the root of both the latin and germanic words are onomatopoeic...

That's cool, but when I say it out loud it sounds like a different word for penis.

The name should just change.

Well, there's more to the world than just the Anglosphere. De Cock is also a popular surname in France and Belgium.

The same person that renamed master to main because slavery..

Yes, me. Telling people I work on "cock" was uncomfortable. It was particularly unwelcoming to women.

Yes - I can also imagine a female programmer not being comfortable when saying that.

Americans mostly as they think the entire world is America.

From what I remember of the discussions on the topic, it's not so much that people are offended by it per se, but there has been many reports of uncomfortable situations from women who use and specifically teach Coq.

Let's be honest, I totally buy that there have been hallway discussions between students about the "Coq teacher" that were wholly inappropriate and should not be encouraged.

What's offensive about a bodypart? Especially if you have one, finding it offensive is rather weird. I, personally, find that whoever came up with the name must have been hilariously innocent, or at least not speaking english. :D

Not sure if you know but the name comes from https://fr.m.wikipedia.org/wiki/Thierry_Coquand

Coq being the first three letters of his name, and also the french name for rooster, the french national emblem.

So yeah, he probably didn't care at all what those letters meant in various languages ( and probably even found the reaction of english natives amusing).

especially if you have one

Rocq was my clear favorite, though I would have picked Roc. It's a real shame that effort seems to have stalled. This is a real barrier yet not widely acknowledged as such.

Reply on news.ycombinator.com