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?
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.
Translation of Python code to Coq | Formal Land (formal.land)