В интересное время мы живем, товарищи! В любой публичной деятельности теперь требуется проявлять изрядную креативность, чтобы обойти все ловушки, лишь бы не задеть случайно кого-нибудь неосторожным словом. То же слово "товарищ" за свою долгую жизнь претерпело несколько смысловых изменений. Изначально товарищи — "торгующие одним товаром". Затем, уже шире, "занимающихся одним делом". Далее, в СССР, когда дело осталось одно на всех — построение коммунизма — "товарищи" стало вообще универсальным обращением, но в современной России сдулось до узкого применения в войсках. А ведь кто-то на "товарища" может и оскорбиться. Например, гусь на свинью — однозначно. Так что заранее прошу уязвимых не спускаться под кат. Потому что речь пойдет о системе Coq.

Вначале каждый из вас должен решить для себя, что же изображено на логотипе Coq. Запомните ответ — опрос будет в конце поста. Для сомневающихся дам подсказку, что le coq — это по-французски "петух". А ведь кому-то уже всё стало ясно и они негодующе воззвали к обществу: "какого хрена?"

Why is the Coq logo made to look like a penis?

(Почему логотип Coq сделан похожим на пенис?)

В рассылке coq-club этот вопрос нашел живейший отклик: за последнее время там не бывало более активных тем. Что ж, у каждого своя нейронная сеть, и если ее хорошенько натренировать, то в любой картинке можно увидеть что-нибудь на "пе..." (петуха?). "Доктор, да вы просто маньяк какой-то!"

Огонь обсуждения весело потрескивал задорными искрами, пока кто-то умный не догадался, наконец, плеснуть бензинчика: "Да что там логотип! Вы посмотрите, как это по-английски произносится и что означает!!!" Стоит заметить, что Coq — штука серьезная, с тридцатилетней историей, поэтому несмотря на узкую нишу интерактивной проверки доказательств, через Coq прошло довольно много людей. И тут оказалось, что среди них было некоторое количество дам, морально страдавших от этого названия, и чуть было не бросивших сам Coq, формальные методы и науку вообще из-за такого безобразия. От петуха запахло жареным, и лучшим представителям сообщества пришлось броситься на спасение корабля, чтобы срочно латать огромную пробоину, проявляя при этом недюжинную фантазию и ту самую креативность.

Сегодня пришло письмо от Theo Zimmermann — руководителя группы разработки Coq, в котором он рассказал, как у них, наконец-то, открылись глаза и пригласил всех к обсуждению нового имени. В нем участвуют такие столпы, как Benjamin Pierce и Xavier Leroy. Подход обстоятельный, как и принято в академической среде: на рассмотрение выставлено уже восемь десятков вариантов. Но в процессе выясняется, что подобрать сочетание звуков, которое ни в каком языке не будет похоже на сленговое обозначение мужских или женских гениталий или чего-либо с этим связанного, очень и очень сложно. Ведь наши предки были не менее изобретательны в придумывании иносказательных выражений для всего этого.

«В компьютерных науках есть только две сложные проблемы — инвалидация кэша и придумывание названий» -- Фил Карлтон

Удачных всем названий — понятных, четких, красивых и никого не оскорбляющих.

P.S. Теперь открываешь цикл статей "Мягкое введение в Coq...", и уже что-то в названии мерещится... А нет, показалось. Конец рабочей недели все-таки. Приятных выходных!

UPD: Обсуждение переименования Coq на Hacker News - сотни комментариев.