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...", и уже что-то в названии мерещится... А нет, показалось. Конец рабочей недели все-таки. Приятных выходных!

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

    Только зарегистрированные пользователи могут участвовать в опросе. Войдите, пожалуйста.

    Что на логотипе?

    • 5,4%Гриб12
    • 69,4%Петух154
    • 4,0%Что-то неприличное9
    • 21,2%Ерунда какая-то47

    Средняя зарплата в IT

    120 000 ₽/мес.
    Средняя зарплата по всем IT-специализациям на основании 8 924 анкет, за 1-ое пол. 2021 года Узнать свою зарплату
    Реклама
    AdBlock похитил этот баннер, но баннеры не зубы — отрастут

    Подробнее

    Комментарии 30

      +2

      Мне, кстати, название всегда не нравилось. Оно нифига не информативно, и напоминает очередную утилиту для поднятия чего-то там. coq up, coq deploy, coq status. Если бы он назывался как-то типа proof, или fproof, то было бы понятнее. (С плавным превращением в /usr/bin/gproof усилиями одной известной организации, да).

        0
        Увы, придумывание названий — штука непростая. Считается, что в названии Coq скрыто CoC (Calculus of Constructions) и часть фамилии одного из создателей — Thierry Coquand. А язык, который Coq имплементирует, назвали Gallina — это по-испански «курица».
          +10

          Так вот кто такая Галина, которая Бланка. Открытие десятилетия просто:)

            +8

            "Белая курица" с испанского, всё просто. Теперь представьте чувства испанца, когда девушка представляется таким именем.

          0

          А агду тоже надо в proof переименовать?

            0

            Agda, кстати, ближе к названию языка программирования. Наверное, из-за сходства высшего порядка с algol'ом.

              0

              Интересные у вас интерпретации.

                0

                Поток сознания и едва ощутимые ассоциации при прочтении названия.

                0

                Agda по названию, имхо, больше на Ada, чем на Algol похожа)

                  0

                  И это тоже.

              0
              Какие есть языки с информативными именами? Кроме brainfuck только два придумываются: vimscript и emacs lisp
                0

                Я бы назвал fortran, рефал, кумир, whitespace, тот же lisp. Ещё clojure можно притянуть за уши: closure — замыкание, на которых вроде как много чего в этом языке строится, а j — потому что JVM. Можно также HTML и SQL упомянуть, хоть первый и отвечает за разметку. Зато второй Тьюринг-полный

                  0

                  Ну да, если знать расшифровки, то эти языки ±информативные.

                    0

                    Cobol ещё. И Рая. :)

                +4
                Доктор, вы просто картинку неправильно повернули. Надо вот так:

                image
                  0

                  Сделают Le Coq или LeCoq и всё. Вот многие и на родном языке фамилии "Рукосуева" и аналогичные имеют — вот это проблема. Древний анекдот в тему:
                  Два бомжа общаются, один из них по фамилии Козлов, хвастается:


                  • Ты знаешь, меня новые русские знают и очень уважают, даже на "Вы" обращаются!
                  • Как так?
                  • Недавно дорогу переходил, так один один из них передо мной резко затормозил, выскакивает и говорит — "для вас, Козлов, столько пешеходных переходов сделали! А вы тут переходите!"
                    Хорошего настроения!
                    0

                    Переименовали бы в Gallo — и нет проблем! Gallina у них же была уже. Но логотипы бывают и поудачнее..

                      0
                      Пишут что язык Gallo уже есть.
                      0
                      Было бы не плохо, переназовись они простым английским именем — Дик.
                        0
                        На логотипе определённо Трамп.
                          0

                          По-моему, это традиция такая. Вот я не очень верю, что фреймворк Mocha это про чай...

                          0
                          На логотипе шаровый сустав
                            0
                            Знакомый биолог сразу распознал мозжечок.
                            Изображают его так

                            0

                            Ну ладно с лого, его поменять можно легко… Но имя…

                              0

                              Там есть несколько вариантов переименования, в которых coq можно будет считать сокращением и оставить в именах утилит и пакетов, так что может не так уж и страшно. Ну или сделают migration tool.

                              +1

                              Имхо, это всё полная ерунда: название coq — "петух" по-французски, созвучно с "cock" по-английски, что тоже значит петух. Т.е. язык назван по имени известной всем птицы мужского пола, и созвучный вариант по-английски ничем в этом плане не отличается. В чём вообще может быть проблема? Мало ли, что и где используется как эвфемизм к чему-нибудь? Давайте ещё вспомним, что в России (в блатной среде) у слова "петух" есть негативные коннотации. Так можно любое слово рано или поздно заклеймить.


                              А вот логотип действительно так себе. Да ещё и невзрачный. Я, например, до сих пор даже не обращал на него внимания ни на сайте, ни в coqide, и не думал даже, что там что-то осмысленное нарисовано, а не просто бледное пятно какое-то.


                              Зато срубили хайпа. Даже вон на Хабре статью впервые с 2013го года написали!

                                –1

                                Для подсёру всем этим СЖВшным начинаниям имеет смысл сделать расширенный форк с гораздо большей системой команд и назвать его BIGcoq. А ещё эмбеддед-версию для микроконтроллеров smolCoq и версию для вычислений с высокой разрядностью LongCoq :-)

                                0
                                Забавно наблюдать за колебаниями туда-сюда оценок статьи и комментариев, кармы, причем синхронное. На мой взгляд, это демонстрирует не просто поляризованность общества, но и какую-то непримиримость. И вот это очень плохо. Как мы научимся понимать друг друга? Я стараюсь услышать и понять разные точки зрения. Если что-то сделал не так — поясните, учту в будущем.

                                Несмотря на то, что я описал ситуацию в шутливых тонах, ситуация с Coq ясна: люди серьезно относятся к мнению сообщества и готовы обсуждать даже такие щекотливые темы в поисках консенсуса. Если пробежаться по аргументам сторон За и Против, то картина примерно такая:

                                З-1: Наша название — это наследие/история!
                                П-1: Но оно может служить барьером для новых людей, вступающих в сообщество.
                                3-2: Нам просто не следует хихикать над глупыми словами, и всё.
                                П-2: Люди стесняются говорить Coq в разговоре, ведущемся по-английски.
                                З-3: Coq был разработан во Франции, где это название вполне осмысленно. Мы же не меняем английские слова из-за того, что они плохо звучат в других языках.
                                П-3: Да, потому что английский — основной язык научной коммуникации.

                                Это — диалог. И сторонники нынешнего названия сами признаются, что недооценивали важность аспектов П-1 и П-2 и ради них готовы пойти на уступки. В интернете всегда кто-то неправ, но лучше ведь жить дружно. Как раз пришла хорошая новость из другой щекотливой истории: Столлман извинился за свое поведение, и его не исключили из FSF.
                                  0
                                  Вы посмотрите, как это по-английски произносится и что означает.

                                  Выше писали, что английский то cock — тоже петух.


                                  При этом cocktail или cockroach(DB) людей не смущает.


                                  P.S.: А вот по-русски — повар на корабле.

                                  Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                  Самое читаемое