[Функциональное программирование, Управление сообществом] Coq — не порок
Автор
Сообщение
news_bot ®
Стаж: 6 лет 4 месяца
Сообщений: 27286
В интересное время мы живем, товарищи! В любой публичной деятельности теперь требуется проявлять изрядную креативность, чтобы обойти все ловушки, лишь бы не задеть случайно кого-нибудь неосторожным словом. То же слово "товарищ" за свою долгую жизнь претерпело несколько смысловых изменений. Изначально товарищи — "торгующие одним товаром". Затем, уже шире, "занимающихся одним делом". Далее, в СССР, когда дело осталось одно на всех — построение коммунизма — "товарищи" стало вообще универсальным обращением, но в современной России сдулось до узкого применения в войсках. А ведь кто-то на "товарища" может и оскорбиться. Например, гусь на свинью — однозначно. Так что заранее прошу уязвимых не спускаться под кат. Потому что речь пойдет о системе 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...", и уже что-то в названии мерещится... А нет, показалось. Конец рабочей недели все-таки. Приятных выходных!
===========
Источник:
habr.com
===========
Похожие новости:
- [Управление сообществом, Управление продуктом, Законодательство в IT, Бизнес-модели, IT-компании] Uber запретил калифорнийским водителям устанавливать свои цены
- [Haskell, Функциональное программирование] Змейка на Haskell с циклом Гамильтона
- [Управление сообществом, Управление e-commerce, Управление продуктом, Финансы в IT, IT-компании] «Алиэкспресс» впервые раскрыл обороты своего российского бизнеса
- [Управление сообществом, Управление e-commerce, Управление продуктом, Управление медиа, Социальные сети и сообщества] А вы используете профайлинг?
- [GitHub, Управление сообществом] Monthly tech community virtual meetings for the Russian-speaking audience/Ежемесячные встречи русскоязычного сообщества
- [Управление сообществом, Научно-популярное, Социальные сети и сообщества, Здоровье] Кто любит возмущаться (перевод)
- [Управление сообществом, Законодательство в IT, Транспорт, IT-компании] «Яндекс» запустил аналог больничных для водителей и курьеров
- [Разработка веб-сайтов, Программирование, Haskell, Функциональное программирование] Создаем веб-приложение на Haskell с использованием Reflex. Часть 2
- [Big Data, Accessibility, Машинное обучение, Искусственный интеллект] Дискриминация в алгоритмах ML существует — и нет, это не либеральные сказки
- [Управление сообществом, Научно-популярное] Сколько радиолюбителей в России?
Теги для поиска: #_funktsionalnoe_programmirovanie (Функциональное программирование), #_upravlenie_soobschestvom (Управление сообществом), #_coq, #_etika (этика), #_politkorrektnost (политкорректность), #_sjw, #_naming, #_18+, #_pjatnitsa (пятница), #_funktsionalnoe_programmirovanie (
Функциональное программирование
), #_upravlenie_soobschestvom (
Управление сообществом
)
Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Текущее время: 20-Июн 00:39
Часовой пояс: UTC + 5
| Автор | Сообщение |
|---|---|
|
news_bot ®
Стаж: 6 лет 4 месяца |
|
|
В интересное время мы живем, товарищи! В любой публичной деятельности теперь требуется проявлять изрядную креативность, чтобы обойти все ловушки, лишь бы не задеть случайно кого-нибудь неосторожным словом. То же слово "товарищ" за свою долгую жизнь претерпело несколько смысловых изменений. Изначально товарищи — "торгующие одним товаром". Затем, уже шире, "занимающихся одним делом". Далее, в СССР, когда дело осталось одно на всех — построение коммунизма — "товарищи" стало вообще универсальным обращением, но в современной России сдулось до узкого применения в войсках. А ведь кто-то на "товарища" может и оскорбиться. Например, гусь на свинью — однозначно. Так что заранее прошу уязвимых не спускаться под кат. Потому что речь пойдет о системе 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. Подход обстоятельный, как и принято в академической среде: на рассмотрение выставлено уже восемь десятков вариантов. Но в процессе выясняется, что подобрать сочетание звуков, которое ни в каком языке не будет похоже на сленговое обозначение мужских или женских гениталий или чего-либо с этим связанного, очень и очень сложно. Ведь наши предки были не менее изобретательны в придумывании иносказательных выражений для всего этого. «В компьютерных науках есть только две сложные проблемы — инвалидация кэша и придумывание названий» -- Фил Карлтон
=========== Источник: habr.com =========== Похожие новости:
Функциональное программирование ), #_upravlenie_soobschestvom ( Управление сообществом ) |
|
Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Текущее время: 20-Июн 00:39
Часовой пояс: UTC + 5