Coq theorem prover is now called Rocq

#1

Post by rwmj » Wed, Apr 15, 2026, 6:40 PM UTC

Re: Coq theorem prover is now called Rocq

#2

Post by nz » Sat, Apr 18, 2026, 12:34 AM UTC

It's good to see that they have chosen a name that has a much more obvious and less confusing spelling.

#3

Post by yodon » Sat, Apr 18, 2026, 12:35 AM UTC

[flagged]

#4

Post by booleandilemma » Sat, Apr 18, 2026, 12:37 AM UTC

Calling it rocq makes it seem harder.

#5

Post by wk_end » Sat, Apr 18, 2026, 12:37 AM UTC

They made this change a couple of years back, didn’t they?

#6

Post by miningape » Sat, Apr 18, 2026, 12:39 AM UTC

I prefer the old name, it was much more memorable because it's funny.

"Yeah I'm playing with my Coq to try and get it working again"

#7

Post by mcluck » Sat, Apr 18, 2026, 12:43 AM UTC

Thank goodness. It's been impossible to talk about Coq to people who don't already know what it is.

#8

Post by mcdonje » Sat, Apr 18, 2026, 12:43 AM UTC

While some may lament the departure of the phallus bird, nobody can be sad about the arrival of the giant fierce mythical bird.

#9

Post by gnabgib » Sat, Apr 18, 2026, 12:46 AM UTC

(2022) Previous discussions

#10

Post by fargle » Sat, Apr 18, 2026, 12:46 AM UTC

why did they find the need to rename this? Am i missing something?