6 ms·

Functional Programming in Coq

65 points by atan2 3y ago

turtleyacht 3y ago
Volume 2: Programming Language Foundations https://softwarefoundations.cis.upenn.edu/plf-current/index.html https://softwarefoundations.cis.upenn.edu/plf-current/index.... Volume 3: Verified Functional Algorithms https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index.... Volume 4: QuickChick: Property-Based Testing in Coq https://softwarefoundations.cis.upenn.edu/qc-current/index.html https://softwarefoundations.cis.upenn.edu/qc-current/index.h... Volume 5: Verifiable C https://softwarefoundations.cis.upenn.edu/vc-current/index.html https://softwarefoundations.cis.upenn.edu/vc-current/index.h... Volume 6: Separation Logic Foundations https://softwarefoundations.cis.upenn.edu/slf-current/index.html https://softwarefoundations.cis.upenn.edu/slf-current/index....
harveywi 3y ago
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 https://github.com/coq/coq/wiki/Alternative-names [2] https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3o%E1%B5%83q https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3...
- mathisfun123 3y ago
  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.
  - phillipcarter 3y ago
    > 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.
    - kerkeslager 3y ago
      It's a problem for those people, and the solution is to grow up. Why should adults care?
      - Capricorn2481 3y ago
        Because nobody wants to say they program in cock
        thefz 3y ago
        1- Languages other than English exist, deal with it 2- Grow up 3- Say "cee-oh-queue"
        erichocean 3y ago
        > 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.
        loupol 3y ago
        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.
    - mathisfun123 3y ago
      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?
      - adultSwim 3y ago
        Try saying the word "pussy" repeatedly in a business or technical conversation.
  - deleted 3y ago
    [deleted]
  - deleted 3y ago
    [deleted]
  - moi2388 3y ago
    The same person that renamed master to main because slavery..
    - adultSwim 3y ago
      Yes, me. Telling people I work on "cock" was uncomfortable. It was particularly unwelcoming to women.
      - barbarbar 3y ago
        Yes - I can also imagine a female programmer not being comfortable when saying that.
  - thefz 3y ago
    Americans mostly as they think the entire world is America.
  - deredede 3y ago
    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.
- deleted 3y ago
  [deleted]
- MrYellowP 3y ago
  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
  - bsaul 3y ago
    Not sure if you know but the name comes from https://fr.m.wikipedia.org/wiki/Thierry_Coquand 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).
  - adultSwim 3y ago
    especially if you have one
- adultSwim 3y ago
  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.
JonChesterfield 3y ago
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.
- deterministic 3y ago
  CompCert is a good example of Coq used to develop complex commercial proven correct software.

65 points by atan2 3y ago

Volume 2: Programming Language Foundations https://softwarefoundations.cis.upenn.edu/plf-current/index.html https://softwarefoundations.cis.upenn.edu/plf-current/index.... Volume 3: Verified Functional Algorithms https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index.... Volume 4: QuickChick: Property-Based Testing in Coq https://softwarefoundations.cis.upenn.edu/qc-current/index.html https://softwarefoundations.cis.upenn.edu/qc-current/index.h... Volume 5: Verifiable C https://softwarefoundations.cis.upenn.edu/vc-current/index.html https://softwarefoundations.cis.upenn.edu/vc-current/index.h... Volume 6: Separation Logic Foundations https://softwarefoundations.cis.upenn.edu/slf-current/index.html https://softwarefoundations.cis.upenn.edu/slf-current/index....

harveywi 3y ago

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 https://github.com/coq/coq/wiki/Alternative-names [2] https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3o%E1%B5%83q https://github.com/coq/coq/wiki/Alternative-names#c%E1%B5%A3...

mathisfun123 3y ago
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.
- phillipcarter 3y ago
  > 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.
  - kerkeslager 3y ago
    It's a problem for those people, and the solution is to grow up. Why should adults care?
    - Capricorn2481 3y ago
      Because nobody wants to say they program in cock
      - thefz 3y ago
        1- Languages other than English exist, deal with it 2- Grow up 3- Say "cee-oh-queue"
        erichocean 3y ago
        > 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.
      - loupol 3y ago
        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.
  - mathisfun123 3y ago
    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?
    - adultSwim 3y ago
      Try saying the word "pussy" repeatedly in a business or technical conversation.
- deleted 3y ago
  [deleted]
- deleted 3y ago
  [deleted]
- moi2388 3y ago
  The same person that renamed master to main because slavery..
  - adultSwim 3y ago
    Yes, me. Telling people I work on "cock" was uncomfortable. It was particularly unwelcoming to women.
    - barbarbar 3y ago
      Yes - I can also imagine a female programmer not being comfortable when saying that.
- thefz 3y ago
  Americans mostly as they think the entire world is America.
- deredede 3y ago
  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.
deleted 3y ago
[deleted]
MrYellowP 3y ago
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
- bsaul 3y ago
  Not sure if you know but the name comes from https://fr.m.wikipedia.org/wiki/Thierry_Coquand 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).
- adultSwim 3y ago
  especially if you have one
adultSwim 3y ago
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.

JonChesterfield 3y ago

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.

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