Coq — не порок
В интересное время мы живем, товарищи! В любой публичной деятельности теперь требуется проявлять изрядную креативность, чтобы обойти все ловушки, лишь бы не задеть случайно кого-нибудь неосторожным словом. То же слово «товарищ» за свою долгую жизнь претерпело несколько смысловых изменений. Изначально товарищи — «торгующие одним товаром». Затем, уже шире, «занимающихся одним делом». Далее, в СССР, когда дело осталось одно на всех — построение коммунизма — «товарищи» стало вообще универсальным обращением, но в современной России сдулось до узкого применения в войсках. А ведь кто-то на «товарища» может и оскорбиться. Например, гусь на свинью — однозначно. Так что заранее прошу уязвимых не спускаться под кат. Потому что речь пойдет о системе Coq.
Вначале каждый из вас должен решить для себя, что же изображено на логотипе Coq. Запомните ответ — опрос будет в конце поста. Для сомневающихся дам подсказку, что le coq — это по-французски «петух». А ведь кому-то уже всё стало ясно и они негодующе воззвали к обществу: «какого хрена?»
Why is the Coq logo made to look like a penis?
(Почему логотип Coq сделан похожим на пенис?)
В рассылке coq-club этот вопрос нашел живейший отклик: за последнее время там не бывало более активных тем. Что ж, у каждого своя нейронная сеть, и если ее хорошенько натренировать, то в любой картинке можно увидеть что-нибудь на «пе…» (петуха?). «Доктор, да вы просто маньяк какой-то!»
Огонь обсуждения весело потрескивал задорными искрами, пока кто-то умный не догадался, наконец, плеснуть бензинчика: «Да что там логотип! Вы посмотрите, как это по-английски произносится и что означает!!!» Стоит заметить, что Coq — штука серьезная, с тридцатилетней историей, поэтому несмотря на узкую нишу интерактивной проверки доказательств, через Coq прошло довольно много людей. И тут оказалось, что среди них было некоторое количество дам, морально страдавших от этого названия, и чуть было не бросивших сам Coq, формальные методы и науку вообще из-за такого безобразия. От петуха запахло жареным, и лучшим представителям сообщества пришлось броситься на спасение корабля, чтобы срочно латать огромную пробоину, проявляя при этом недюжинную фантазию и ту самую креативность.
Сегодня пришло письмо от Théo Zimmermann — руководителя группы разработки Coq, в котором он рассказал, как у них, наконец-то, открылись глаза и пригласил всех к обсуждению нового имени. В нем участвуют такие столпы, как Benjamin Pierce и Xavier Leroy. Подход обстоятельный, как и принято в академической среде: на рассмотрение выставлено уже восемь десятков вариантов. Но в процессе выясняется, что подобрать сочетание звуков, которое ни в каком языке не будет похоже на сленговое обозначение мужских или женских гениталий или чего-либо с этим связанного, очень и очень сложно. Ведь наши предки были не менее изобретательны в придумывании иносказательных выражений для всего этого.
«В компьютерных науках есть только две сложные проблемы — инвалидация кэша и придумывание названий» — Фил Карлтон
Удачных всем названий — понятных, четких, красивых и никого не обижающих.
P.S. Теперь открываешь цикл статей «Мягкое введение в Coq…», и уже что-то в названии мерещится… А нет, показалось. Конец рабочей недели все-таки. Приятных выходных!
