• ∃∀λ@programming.dev
    link
    fedilink
    arrow-up
    3
    ·
    21 hours ago

    Another example is Coq, the interactive theorem prover, named after CoC, an abbreviation for calculus constructions, the type theory on which Coq is based, and the co-creator Thierry Coquand in whose native language (French) coq has no sexual connotation and is simply the word for rooster (male chicken).

    I have just now seen on Wikipedia to gather this information that it was renamed to Rocq last year after 41 years.

    https://github.com/rocq-prover/rocq/wiki/Alternative-names