Skip to content
  • Categories
  • Recent
  • Tags
  • Popular
  • Users
  • Groups
Skins
  • Light
  • Cerulean
  • Cosmo
  • Flatly
  • Journal
  • Litera
  • Lumen
  • Lux
  • Materia
  • Minty
  • Morph
  • Pulse
  • Sandstone
  • Simplex
  • Sketchy
  • Spacelab
  • United
  • Yeti
  • Zephyr
  • Dark
  • Cyborg
  • Darkly
  • Quartz
  • Slate
  • Solar
  • Superhero
  • Vapor

  • Default (No Skin)
  • No Skin
Collapse

The New Coffee Room

  1. TNCR
  2. General Discussion
  3. The problem with Coq

The problem with Coq

Scheduled Pinned Locked Moved General Discussion
4 Posts 4 Posters 37 Views
  • Oldest to Newest
  • Newest to Oldest
  • Most Votes
Reply
  • Reply as topic
Log in to reply
This topic has been deleted. Only users with topic management privileges can see it.
  • KlausK Offline
    KlausK Offline
    Klaus
    wrote on last edited by Klaus
    #1

    There's a famous tool for theorem proving which is called "Coq", after the French name for rooster and also after it's name inventor, whose first name is Coquand.

    They've become sick of the countless jokes that resulted from that name, so they are thinking of a better one. There's some bullshit "diversity, equity, inclusion" arguments, too, of course.

    https://github.com/coq/coq/wiki/Alternative-names
    https://www.theregister.com/2021/06/15/coq_programming_language_change/

    Turns out that one of the main problem is that basically every word is in some language a slang word for penis.

    Doctor PhibesD 1 Reply Last reply
    • MikM Offline
      MikM Offline
      Mik
      wrote on last edited by
      #2

      🤣

      “I am fond of pigs. Dogs look up to us. Cats look down on us. Pigs treat us as equals.” ~Winston S. Churchill

      1 Reply Last reply
      • KlausK Klaus

        There's a famous tool for theorem proving which is called "Coq", after the French name for rooster and also after it's name inventor, whose first name is Coquand.

        They've become sick of the countless jokes that resulted from that name, so they are thinking of a better one. There's some bullshit "diversity, equity, inclusion" arguments, too, of course.

        https://github.com/coq/coq/wiki/Alternative-names
        https://www.theregister.com/2021/06/15/coq_programming_language_change/

        Turns out that one of the main problem is that basically every word is in some language a slang word for penis.

        Doctor PhibesD Offline
        Doctor PhibesD Offline
        Doctor Phibes
        wrote on last edited by Doctor Phibes
        #3

        @klaus said in The problem with Coq:

        Turns out that one of the main problem is that basically every word is in some language a slang word for penis.

        You're pulling my Klaus, as they say in Wales.

        I was only joking

        1 Reply Last reply
        • Catseye3C Offline
          Catseye3C Offline
          Catseye3
          wrote on last edited by
          #4

          Buncha Coquand bull, if you ask me.

          Success is measured by your discipline and inner peace. – Mike Ditka

          1 Reply Last reply
          Reply
          • Reply as topic
          Log in to reply
          • Oldest to Newest
          • Newest to Oldest
          • Most Votes


          • Login

          • Don't have an account? Register

          • Login or register to search.
          • First post
            Last post
          0
          • Categories
          • Recent
          • Tags
          • Popular
          • Users
          • Groups