• rutrum@lm.paradisus.day
      link
      fedilink
      arrow-up
      3
      ·
      6 months ago

      Its pronounced “coke” I believe. Its named after the french mathematician Thierry Coquand. Apparently coq is also a name for rooster. According to wikipedia, computer science in France frequently names things after animals? Idk dont we all?

    • sugar_in_your_tea@sh.itjust.works
      link
      fedilink
      arrow-up
      3
      ·
      edit-2
      6 months ago

      Coq. They just want to Python and Coq interchangeably so they can prove their Python/Coq is free of bugs. It’s just a way to get your Python/Coq tested to ensure it’s clean to use, and ideally it would be tested frequently.

  • rutrum@lm.paradisus.day
    link
    fedilink
    arrow-up
    1
    ·
    6 months ago

    I like the motivation of the problem: use mathematical rigor to guaruntee something that is complex and certainty is a requirement, like crypotcurrency, is valid.