CoqがThe Rocq Proverに改名
Coqが始まった場所（INRIA-Rocquencourt）
30年以上の研究の成果
Thierry CoquandとGérard Huetによって1984年に開始
メリット
短い名前
歴史との強い関連
「c」「o」「q」の文字を保持
英語とフランス語で「rock」と「roc」（硬い石）に近い
良い連想（bedrock）
「Coq hacker => Rocq star」のような言葉遊びの可能性
神話の鳥「Roc」に関連
実用性
ネイティブスピーカーにとって発音しやすい
良い意味合い（堅実さ、強さ）
Googleでのヒットが少ない
注意点
発音に混乱が生じる可能性
頭字語として読む場合の提案: Real-world maths, Objective-camel implemented, CQ based proof assistant
「Roc」という未発表のプログラミング言語が存在する 改名時に行われた議論
元のCoqの名前の由来
フランス語の「rooster」(雄鶏)
問題
英語スラング「cock」と似てる
一般人との会話が難しくなる
ハラスメントが起きたこともあるらしい