URL: https://www.opennet.dev/cgi-bin/openforum/vsluhboard.cgi
Форум: vsluhforumID3
Нить номер: 123889
[ Назад ]
Исходное сообщение
"Инструментарий для доказательства теорем Coq рассматривает возможность смены названия"
Отправлено opennews , 09-Апр-21 23:22 
Инструментарий для доказательства теорем Coq рассматривает возможность смены названия. Причина: для англофонов слова "coq" и "cock" (сленговое название мужского полового органа) звучат похоже, и некоторые пользователи-женщины, сталкивались с двусмысленными шутками при использовании названия в устной речи. Само же название языка Coq произошло от фамилии одного из разработчиков, Thierry Coquand. Сходство звучания Coq и Cock (англ. петух) уже обыгрывалось в проекте: язык, используемый для описания конструкций, называется Gallina (лат. курица)...

Подробнее: https://www.opennet.dev/opennews/art.shtml?num=54933

Содержание
Сообщения в этом обсуждении
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Hedgehog , 09-Апр-21 23:22 
Зачем эта очень важная "новость" нужна именно на опеннете?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Антифрактал , 09-Апр-21 23:23 
чтобы ты был в курсе, как мир сходит с ума, подстраиваясь под англицизмы
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 00:27 
Вернее подстраиваясь под впечатлительных подростков, феминисток, гомосеков и прочих психически неустойчивых личностей
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:01 
анон, ну не смешно вообще. Если ьы он назывался hui - у нас бы точно так же измывались над ним.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено RomanCh , 11-Апр-21 09:50 
Почему "бы"? Пожалуйста: https://gethue.com/

PS Кстати работает оно вполне соответствуще своему названию (для русскоговорящих)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено ого , 11-Апр-21 19:43 
но истерить до смены названия не стали бы.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Wine_O_Feliya , 12-Апр-21 15:11 
Это как с проектом "pydora"? Где-то в тексте на PyPI можно засвидетельствовать " [..] config file pydora [..]"
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Ordu , 10-Апр-21 10:38 
Обидно, да? Под впечатлительных подростков, феминисток и гомосеков они подстраиваются, а под впечатлительных опеннетовцев, которые до сих пор триггерятся по поводу Pidora они не подстраиваются.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 13:42 
Так мы просто пошутили и посмеялись, но никто не поднимал серьезно вопрос о переименование.
Этим адекватный человек и отличается от психически больного - тем что тихо хихикает с друзьями, а не выносит подобные вопросы на всеобщее обсуждение.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Ordu , 10-Апр-21 15:04 
А когда людям надоедает это хихиканье "адекватных" и "психически здоровых" при каждом упоминании их проекта, они делают что? Переименовывают проект, чтобы не хихикали.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 12-Апр-21 17:26 
Новость читал? Не автору надоело хихканье, иначе он бы так не назвал. А "некоторые пользователи-женщины" АБИДЕЛИСЬ на "двумысленные шутки".

Кстати, если в твоём нике заменить первые 4 буквы на c, o, c и k - тоже получится АБИДНОЕ двусмысленное слово! Я оскорблён! Переименуйся, пожалуйста, иначе я тебе травлю устрою :)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Ordu , 12-Апр-21 18:27 
> Новость читал? Не автору надоело хихканье, иначе он бы так не назвал.
> А "некоторые пользователи-женщины" АБИДЕЛИСЬ на "двумысленные шутки".

Да. "Адекватные" и "психически здоровые" люди отпускали "двусмысленные шутки" в отношении женщин, работавших с coq. Их это задрало, автор вошёл в положение, и согласился с тем, что стоит переименовать.

> Кстати, если в твоём нике заменить первые 4 буквы на c, o,
> c и k - тоже получится АБИДНОЕ двусмысленное слово! Я оскорблён!
> Переименуйся, пожалуйста, иначе я тебе травлю устрою :)

Устраивай! Я люблю, когда меня травят "адекватные" и "психически здоровые". Если это поможет тебе решиться на травлю, я могу попросить Шигорина сменить мне ник на cock.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:40 
> мир сходит с ума

    CKEditor — свободный WYSIWYG-редактор

    До версии 3.0 назывался FCKeditor («FCK» от имени создателя редактора,
    Frederico Caldeira Knabben), но сменил имя чтобы не ассоциироваться
    с распространённым в английском языке ругательством

>   CKEditor 3.0 is here!
>   by Frederico Knabben
>   Posted on 2009-08-21
>   Posted on 2009-08-21
>   Posted on 2009-08-21

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Неа , 10-Апр-21 09:26 
Этот редактор такое же гуано, как и аргументы про Coq
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:03 
А как тебе ЁбРедактор? Сколько у нас ржали над ё-мобилем? Или это другое? Свое как грица не пахнет?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Noname , 13-Апр-21 15:52 
> ЁбРедактор

Vi как vi, чё бухтеть- то?

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 06:47 
Язык международного общения - английский. Не китайский и не русский как некоторым здесь не хотелось. Если авторы данного инструментария хотят популярности в мировом масштабе, то озаботиться вопросом благозвучного названия естественно.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Тот_Самый_Анонимус , 10-Апр-21 06:56 
>Язык международного общения - английский.

Однако, в основном, только носители этого недоязыка понимают эту игру слов. Я вот не знаю всего множества жаргонизмов, которыми носители языка называют *уй. И даже запоминать не собираюсь. И автора этого продукта это не парило достаточно продолжительное время. Просто сейчас истерия в тренде.

>Не китайский и не русский как некоторым здесь не хотелось.

Это тоже языки международного общения, как бы вам не хотелось иного.

> Если авторы данного инструментария хотят популярности в мировом масштабе

Не в мировом масштабе, а популярности среди истеричек, которым везде *уй мерещится (даже в хлебобулочных изделиях продолговатой формы). Гимпу вон плевать на такое. Идите, почитайте им лекции, как распростанять свой продукт по миру.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 10-Апр-21 07:37 
> Это тоже языки международного общения, как бы вам не хотелось иного.

Про китайский - согласен, хотя это больше дело будущего.

А на русском ты разве что в вестник Бобруйского университета сможешь писать.  И то - пока.

> Гимпу вон плевать на такое.

Вопрос времени когда его достанут.

Тут вот все просто: M$, гранты.  Взяли под козырек, на всякий случай.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено RomanCh , 11-Апр-21 09:54 
> А на русском ты разве что в вестник Бобруйского университета сможешь писать.

Нет. В ООН на самом деле тоже можно: https://www.un.org/ru/sections/about-un/official-languages/i...

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 11-Апр-21 12:15 
Ну, ООН - известна своей научностью.  Там даже Эйлер состоял.

Нет, вру.  Эйлер в Петербургской, Берлинской и Парижской академиях состоял.  А в ООН состоят всякие шейхи, работорговцы, вчерашние людоеды и проч. человеческий мусор.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено RomanCh , 11-Апр-21 12:44 
> и проч. человеческий мусор.

Уууу... Понятно.


"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:04 
> этого недоязыка

и 7 лайкосов.
Как грица угадай в какой стране живут нацисты, расисты и шовинисты.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено RomanCh , 11-Апр-21 09:57 
> Как грица угадай в какой стране живут нацисты, расисты и шовинисты.

Во всех. К сожалению.

Но вообще про проблемы английского я в целом согласен, в силу того что он совершенно не фонетический. Т.е. невозможно зная алфавит правильно прочитать слова. Хуже того, носители языка сами не всегда уверены как произносится фамилия того или иного коллеги, если она сильно отличается от наиболее распространённых. При работе в международных компаниях это очень сильно доставляет, если честно.

И самое плохое, что никто ничего с этим не собирается делать.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 11-Апр-21 12:16 
А зачем с этим что-то делать?  Есть эсперанто.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено RomanCh , 11-Апр-21 12:45 
> А зачем с этим что-то делать?  Есть эсперанто.

И как у вас с ним? Регулярно практикуете? Научные статьи в мухосранскую академию эсперанто пишете?

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Noname , 13-Апр-21 15:56 
- Ты же робот, имитация жизни! Может робот способен написать симфонию?
- Будто ты можешь.

занавес

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Доктор психушки , 12-Апр-21 17:59 
> нацисты, расисты и шовинисты

Какой вы агрессивный, батенька! Будем лечиться! Смирительную рубашку на него! Тащите на процедуры

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Noname , 13-Апр-21 15:58 
А что не так?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 12-Апр-21 18:02 
> Как грица угадай в какой стране живут нацисты, расисты и шовинисты.

Чувачок, тебе реально нужно как минимум успокоительного попить. Когда везде мерещатся нацисты и расисты - это ненормально.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 06:02 
> Зачем эта очень важная "новость" нужна именно на опеннете?

Чтобы через Интерпол его экстрадировать в РФ и посадить здесь в тюрьму за оскорбление чувств, с готовой кликухой.

Нечего проектам дурацкие названия придумывать!

И нужно немедленно составить базу знаний по оскорбительным словам всех языков Мира, чтобы нейросеть сразу определяла, можно такое название использовать или нет.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 10-Апр-21 15:41 
> составить базу знаний по оскорбительным словам всех языков Мира,
> чтобы нейросеть сразу определяла, можно такое название использовать или нет.

есть мнение, что НИКАКОЕ название не пройдет через такую нейросеть.
везде будет значимая подстрока или омоним или еще чего-то типа
оскорбления беременных негролебезьянок.

ps: например SemenSemenych777 точно не пройдет. потомучто.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 06:57 
"СеменСеменыч777" бы не прошел прежде всего в СССР, ежели бы тот не распался. Потому что уничижительный для Советского человека ник.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 10-Апр-21 06:54 
Ну а при каком обстоятельстве посетители opennetу впринципе могли бы узнать, что там не только "негров линчуют", но и формализацией математики занимаются на уровне, за которым уже целым институтам РАН не угнаться?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Тот_Самый_Анонимус , 10-Апр-21 06:59 
>но и формализацией математики занимаются на уровне, за которым уже целым институтам РАН не угнаться?

Ради красного словца не пожалеем и отца? Разумеется подтверждения своим словм вы не приведёте.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 10-Апр-21 07:06 
Ну, представленного общественности инструмента уровня Coq разработано было не было.  Не говоря уже о получении к-л известных формальных доказательств с ним...
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено НеОН , 12-Апр-21 17:23 
Слава морфу! Слава 404!
Защифрованное послание, которое поймут лишь избранные!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:22 
Hey bro nice Coq
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:43 
Nice coq, awesome balls.
terminator.jpg
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено iPony129412 , 10-Апр-21 07:04 
https://derpicdn.net/img/view/2021/4/2/2584442__safe_artist-...
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Человек под травой , 10-Апр-21 09:25 
Nice coq, swesome proofs.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Wine_O_Feliya , 12-Апр-21 15:13 
Gallina blank'a bool bool
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:22 
Одобряю. Но только если они знали о проблеме с названием, почему назвали язык тоже шуточно - неясно.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:58 
А они в качестве шутки тогда и сделали такое название. Но то было тогда. а сейчас пришли новые разработчики и настали новые времена, когда не шутят.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено пох. , 10-Апр-21 09:21 
Потому что этот Терри совершенно не парится что кто-то на слух воспримет его фамилию как "Петушара". И менять ее не планирует.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Тётка с ведром , 10-Апр-21 10:43 
No fun allowed.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Cradle , 10-Апр-21 00:35 
французы, сэр. Тогда постебались, а теперь боязно стало.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Lex , 10-Апр-21 04:30 
Coq - петух (с франц)
Раньше было модно-молодёжно по дурацки именовать продукт. Не удивлюсь, если те же самые разработчики выросли и внезапно поняли, что это скорее тупо, чем юморнО.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено пох. , 10-Апр-21 09:22 
А фамилию им тоже выросши внезапно сменить? А то ж вызывает нездоровые ассоциации.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:10 
лол блин. Ты правда считаешь что петух имеет негативную коннотацию во Франции? Петушиная субкультура - она же географически находится в других местах.

/мимо подписчик на мопса

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Lex , 10-Апр-21 13:58 
> лол блин. Ты правда считаешь что петух имеет негативную коннотацию во Франции?
> Петушиная субкультура - она же географически находится в других местах.

Я лишь говорю, что кок - петух с французского. И что раньше была мода черти как называть проги.
Вот ты можешь по названию проги - «петух», однозначно догадаться что так называется инструментарий для доказательства теорем ?

У фрацузов и жителей южной европы своя субкультура петушиная.. с той лишь разницей, что «петух» там скорее комплимент..

И кОков тех полным-полно. Почитать, хотя бы, историю открытия металла галлия.. французом лекоком из г. коньяк


"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 07:01 
> Вот ты можешь по названию проги - «петух», однозначно догадаться что так называется инструментарий для доказательства теорем ?

Вот ты можешь по названию проги - «Windows», однозначно догадаться что так называется операционная система?

Вот ты можешь по названию проги - «Inkscape», однозначно догадаться что так называется инструментарий для векторной графики ?

Вот ты можешь по названию проги - «WinRar», однозначно догадаться что так называется инструментарий для архивирования ?

Вот ты можешь по названию проги - «Photoshop», однозначно догадаться что так называется графический редактор ?

ну ты понял...

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Lex , 11-Апр-21 14:42 
> Вот ты можешь по названию проги - «Windows», однозначно догадаться что так
> называется операционная система?

Окна.. экраны. Какая-то взаимосвязь есть

> Вот ты можешь по названию проги - «Inkscape», однозначно догадаться что так
> называется инструментарий для векторной графики ?

ink - чернила. Есть какая-то связь с рисованием и "рисовалкой"

> Вот ты можешь по названию проги - «WinRar», однозначно догадаться что так
> называется инструментарий для архивирования ?

WinRar - [Rar]-архиватор для [Win]dows. Связь есть.
Rar - формат сжатия, разработанный Евгением Рошалом. И название - [Р]ошал [Ар]хиватор. Т.е даже в названии формата упоминается, для чего он.

> Вот ты можешь по названию проги - «Photoshop», однозначно догадаться что так
> называется графический редактор ?

Изображения, фотографии.. какая-то связь есть

> ну ты понял...

Ну вообще-то нет.
Так какая связь между названием Петух( в лучшем случае ) и инструментарием для доказательства теорем ?

Не видеоредактором, не подборкой горячих видосиков 18+, не инструментарием восстановления поврежденных древних надписей и изображений, разработанного во Франции, не ПО для автоматизации фермы или чего-то еще подобного.. а, черт возьми,  инструментарием для доказательства теорем.
Конечно, можно тупо сослаться на три первых буквы фамилии ОДНОГО ИЗ разработчиков ( не удивлюсь, если "совершенно случайно" именно того, с фамилией которого получалось не "пет" / "сти" / "мих" / "гам" / итп, а именно кок ), но это будет слишком тупо.


"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Michael Shigorin , 11-Апр-21 21:25 
> Rar - формат сжатия, разработанный Евгением Рошалом. И название - [Р]ошал [Ар]хиватор.

[...]
> Конечно, можно тупо сослаться на три первых буквы фамилии ОДНОГО ИЗ разработчиков

Мнэээ... Вы точно с собой дискутировали? :)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Lex , 12-Апр-21 11:21 
>> Конечно, можно тупо сослаться на три первых буквы фамилии ОДНОГО ИЗ разработчиков
> Мнэээ... Вы точно с собой дискутировали? :)

Заранее ответил, предвидя очередной тупой вопрос в продолжение не мене тупого срача

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено InuYasha , 11-Апр-21 11:33 
Вообще, FYI, петух во франции - это почти что национальный маскот.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Gogi , 10-Апр-21 11:39 
Представляю, как сейчас краснеет в гробу Джобс со своим.... ха... ЯБЛОКОМ! :)))
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 06:04 
> - неясно.

Пропиарились же.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 12:28 
Потому что в основу Coq положена теория типов "calculus of constructions" (CoC).
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноным , 09-Апр-21 23:22 
При всем этом остается загадка: как до сих пор не сломлен ГИМП?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:23 
Глимпс
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Стас Михайлов , 09-Апр-21 23:51 
Не существует.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 08:51 
Глиномес.
FTGJFIX
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Антифрактал , 09-Апр-21 23:24 
Прокудин им не дает сломаться, поит их воткой. Это стимулирует их моск посылать на хрен всех чересчур умных
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Annoynymous , 09-Апр-21 23:31 
Слава Прокудину!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:07 
Прокудину слава!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:01 
Андрей
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:31 
> загадка

https://www.opennet.dev/opennews/art.shtml?num=51357
https://www.opennet.dev/opennews/art.shtml?num=53602

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноным , 09-Апр-21 23:59 
Форк же, а не переименован
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:22 
Язык Си - первая буква слова cock.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Жорш , 10-Апр-21 01:18 
А rust от ruster - кугут
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Какаянахренразница , 10-Апр-21 11:26 
> кугут

Давненько не слышал этого слова.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:19 
Я прозрел
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Q2W , 10-Апр-21 08:10 
Думаю, низкосортный вообще и сортирный в частности юмор существовал и раньше.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено timur.davletshin , 09-Апр-21 23:32 
Если стеблись, когда называли, то надо продолжать в том же духе. Если у кого-то бомбит, то цель достигнута. Не пойму, почему баб должно от "петушка" бомбить? Я думал, что должно наоборот.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 00:10 
Например, можно назвать πdr.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:10 
> почему баб должно от "петушка" бомбить?

Потому что небритые цветноволосые ненавидят всё, что связано с "мущщинками"

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:14 
вообще не врубаешься. Сидят двое коллег пишут доказательства: парень, девушка. Парень подзывает девушку и говорит, показывая на код на экране и глумливо улыбаясь: "Как тебе мой coq?". Я не знаю ни одной даже условно приличной девушки, даже нашей, которая будет долго терпеть такие шутеечки.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 10-Апр-21 11:26 
> Я не знаю ни одной даже условно
> приличной девушки, даже нашей, которая будет долго терпеть такие шутеечки.

Когда-то в очередной раз сдавал лабу по туннельному эффекту, а наш поток безуспешно этим занимался уже третий месяц. Мне это дело на пальцах накидал один шаман, и я провёл аналогию с сифоном: берём стакан с водой, опускаем трубку; что бы вода преодолела потенциальный барьер, надо... отсосать.

Вот тут я услышал тот самый звук тишины. Вся группа набрала полные лёгкие воздуха, что бы утешиться несчастьем ближнего. У препода от моих слов глаза на лоб полезли. Она выдержала паузу, обвела опешившим взглядом студентов и выдала: "хоть кто-то что-то понял!" Ну а кто полные лёгкие не удержал и взоржал, те ещё пару месяцев искали более подходящее слово.

Так что, друг Горацио, впереди ещё много открытий чудных.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Михрютка , 10-Апр-21 14:12 
тетка в теме. чтобы сдать лабу - надо отсосать.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 11-Апр-21 07:25 
Есть такая штука - шприц для удаления припоя, он же вакуумный оловоотсос, в просторечии "отсосник".  Я с его помощью нерабочий стенд за дипломниками восстановил. За что мне все лабы зачли. ;)
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 07:04 
Ж))))))
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 12:47 
Анатомию иди отмени. Там не только названия, но и картинки показывают неприличные.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено пох. , 12-Апр-21 11:03 
уже ж отменили (точнее, пытались): https://kulturomania.ru/news/item/kommunisty-rossii-prizvali.../

трогательное единство коммуняк и попов ;-)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 12-Апр-21 18:20 
> показывая на код на экране и глумливо улыбаясь: "Как тебе мой coq?"

Какая надуманная ситуация.

Я девушка-программист, и 1) никогда такого рода шутки не встречала, хотя начала работать ещё до массовой истерии обид, когда нравы были свободнее; 2) если б и услышала, просто спокойно проигнорила, и с лёгкой улыбкой приступила бы к критике его coq-а )
Если человек настолько чувствителен, что его такие двусмысленные слова оскорбляют, пусть идёт двор мести, где с ним никто не разговаривает и обидеться не на кого.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено ого , 12-Апр-21 18:56 
ты бы, конечно, предпочёл, чтобы это были два парня, да?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:23 
Вот же неженки блин, бабу коком напугали. Толи наши люди, ковыряются в Zope молча и не хнычут.  
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 10:15 
Так там же уже Grok или что там?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Ag , 10-Апр-21 08:31 
А представьте когда такие проблемы надо будет разруливать авторам учебников и пособий по птицеводству!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено timur.davletshin , 10-Апр-21 08:41 
> А представьте когда такие проблемы надо будет разруливать авторам учебников и пособий
> по птицеводству!

Каплун/пулярка — всё придумано уже.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:35 
А еще надо запретить Code Of Conduct
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Жорш , 10-Апр-21 01:20 
CoC всегда потеха для рубиста
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:41 
Гашина - испанское  слово 😜
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 09-Апр-21 23:50 
Так Галина Бланка это не жена Моисея Бланка? Как теперь жить...
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено cz , 10-Апр-21 01:52 
На испанском "Gallina blanca" - это вообще "Белая курица". Попробуйте пожить с этим.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 10-Апр-21 07:45 
Для Галлов петух тотемная птица, предвестник рассвета.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 13:12 
Он для всех нормальных людей предвестник рассвета. Кроме всяких городских озабоченных с подвортами
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 11-Апр-21 07:46 
Есть версия, что "галлы" и "славяне" -- эдакая лингвистическая калька. Первое родственно с "голос", а второе со "слово". Ныне homo sapiens-ы, а тогда был "человек говорящий".
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 11-Апр-21 09:04 
> Первое родственно с "голос", а второе со "слово"

задорновщина.
я поставил себе за правило - игнорировать любые лингвистические аргументы,
чего и всем рекомендую. потому что поляна очень загажена, и с официальной стороны,
и с альтернативных.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 13-Апр-21 07:11 
> я поставил себе за правило - игнорировать любые лингвистические аргументы,

Заметно, ведь "три топора" - это популярное в некоторых кругах питиё советских времён.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 15-Апр-21 20:20 
>> > я поставил себе за правило - игнорировать любые лингвистические аргументы,
> Заметно, ведь "три топора" - это популярное в некоторых кругах питиё советских
> времён.

не вижу связи. скорее всего её и нет.

ps: анонимусу сменить ник - дело пяти минут. подумайте об этом.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 16-Апр-21 10:06 
>>> > я поставил себе за правило - игнорировать любые лингвистические аргументы,
>> Заметно, ведь "три топора" - это популярное в некоторых кругах питиё советских
>> времён.
> не вижу связи. скорее всего её и нет.
> ps: анонимусу сменить ник - дело пяти минут. подумайте об этом.

я поставил себе за правило - игнорировать любые аргументы

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено n00by , 16-Апр-21 10:07 
>>>> > я поставил себе за правило - игнорировать любые лингвистические аргументы,
>>> Заметно, ведь "три топора" - это популярное в некоторых кругах питиё советских
>>> времён.
>> не вижу связи. скорее всего её и нет.
>> ps: анонимусу сменить ник - дело пяти минут. подумайте об этом.
> я поставил себе за правило - игнорировать любые аргументы

Вот это пральна! ;-)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 00:02 
Но вообще правильно, слишком грубо это. Наверняка все шутят постоянно.

>The name Coq comes from the French word for rooster, CoC (the Calculus of Constructions) and Thierry Coquand, one of the initial authors of Coq

Предлагаю что-нибудь более нейтральное, например, Diq - Development of Information Constuctions (по мотивам оригинала). Подойдёт?

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Дихлофос , 10-Апр-21 00:11 
Предлагаю поменять на Гуч
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено InuYasha , 10-Апр-21 00:34 
There are no easter eggs in Gallina!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Dzen Python , 10-Апр-21 01:12 
Буль-буль!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено InuYasha , 11-Апр-21 11:28 
М-да, у этих анонов нет чувства юмора. )
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Dzen Python , 10-Апр-21 01:11 
Предлагаю вообще не использовать буквы любого алфавита - они все так или иначе входят в оскорбительные, матерные или эвфеместичные слова, которые оскорбляют книггеров и жирофемок.
Предлагаю вообще не использовать цифры - они тоже могут быть оскорбительны: 14-88 или 13-99 оскорбляют антифа, дни рождения самых страшных маньяков, тиранов, комми и шовинистов состоят из цифр и могут оскорбить любого.
Предлагаю вообще не использовать в названиях спецсимволы - аутисты, дисграфики и клинические слабоумные не могут их ни прочитать, не произнести, а это, между прочим, дискриминация и ущемление.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:21 
Концу мир!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Dzen Python , 10-Апр-21 19:54 
Да, майн либен?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Annoynymous , 11-Апр-21 01:41 
> Концу мир!

А миру герцог!

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:12 
Там это... ВВС не собирается предпринимать срочные меры?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Ingener , 10-Апр-21 01:16 
Да. Правильно. "Кок" это как бы ..лен половой. Надо так назвать - Vagee.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:18 
Они там все шутники. Например, язык Agda, цитата из вики
"Agda is named after the Swedish song "Hönan Agda".... which is about a hen named Agda. This alludes to the naming of Coq."
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:20 
А питон этих дам не отпугивает?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 03:22 
Многие его не любят, но многие пользуются - на жалость пробивает, вестимо.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:29 
К чëрту Coq, дамы! Лучше я познакомлю вас со своим Python-ом!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 01:49 
твой питончик не идёт ни в какое сравнение с моей анакондой
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 16:39 
Одноглазой
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено YetAnotherOnanym , 10-Апр-21 02:07 
Chick неплохой вариант.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 02:23 
Могут перейти на кириллицу и больше не будет проблем.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 03:00 
Вечно эти женщины чем-то недовольны
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 06:55 
своей внутренней пустотой, видимо
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Михрютка , 10-Апр-21 18:11 
а ты заполняй чаще. тогда тебе с утра не только пирожков напекут, но и ядро за тебя сконпелируют, хакер грозный.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Annoynymous , 11-Апр-21 12:17 
> а ты заполняй чаще. тогда тебе с утра не только пирожков напекут,
> но и ядро за тебя сконпелируют, хакер грозный.

На редкость дельный совет!

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено anonymous , 10-Апр-21 14:57 
Зачем же так прочерчивать линию между мужчинами и женщинами? На самом деле, большинство мужчин и женщин вообще не в курсе про coq.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 03:31 
Using the creator name's Coquand as Coq's full name

Coq would be viewed as an abbreviation. ...

Talia: I really like this. The only slightly weird thing about it is that he is alive

Ну это как раз решаемая проблема!

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено anonimm , 10-Апр-21 03:58 
Если {an}, n=1,2,... - последовательность, то как политкорректно назвать an?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 04:07 
Ну и что?пусть меняют название, от этого мне не холоднее или теплее.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено nomad__ , 10-Апр-21 06:54 
С 80-х годов существует и не было ни у кого проблем с названием. А тут вдруг появились. Бесноватые и сюда добрались.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено anonymous , 10-Апр-21 15:00 
Ну а ещё не так давно в мире практиковалось рабство и это было традиционно нормальным явлением. И аналогично "ни у кого не было с этим проблем". Мир меняется. Адаптируйтесь ;)
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено nomad__ , 10-Апр-21 15:44 
> Ну а ещё не так давно в мире практиковалось рабство и это
> было традиционно нормальным явлением. И аналогично "ни у кого не было
> с этим проблем". Мир меняется. Адаптируйтесь ;)

Нахрен этот идиотский мир.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 10-Апр-21 15:53 
> ещё не так давно в мире практиковалось рабство

до сих пор практикуется. заключенные те же рабы.

> и это было традиционно нормальным явлением.

и это нормально.

> Мир меняется.

просто вы не знаете мир, в котором живете.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 07:11 
Цинизм - это нормально в отношении других. Как и рабство. А вот когда тебя - это плохо, ооой как плохо.

А вообще отсутствие эмпатии в нашей культуре показывает лишь ее место в культуре Человечества

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 11-Апр-21 08:50 
если выражаться политкорректно: философия и этика как её подраздел - это не ваша сильная сторона. просто смиритесь с этим. по мере накопления жизненного опыта может быть что-то и будет.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 11-Апр-21 08:58 
если неполиткорректно: какой еще "нашей культуре" ? я отказываюсь иметь общую культуру с SJW всех сортов, хипстреней-смузихлебами и половыми извращенцами.

последним я уже готов отказать в биологической принадлежности к виду Homo Sapiens Sapiens, потому что они сломали несколько базовых инстинктов. это уже не люди, "эмпатия" к ним неприменима и вредна.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Michael Shigorin , 11-Апр-21 21:18 
> А вообще отсутствие эмпатии в нашей культуре показывает лишь ее место
> в культуре Человечества

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

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено пох. , 11-Апр-21 16:28 
> до сих пор практикуется. заключенные те же рабы.

Только измельчали что-то, лампочки какие-то устаревшие, мелкошвейное производство в основном тех же роб для самих себя, всякая ерунда короче ненужная и некачественная - а где новые пирамиды?! Где акведуки?! Твою ж двадцать - даже ж поганый БАМ не осилили (его настоящие рабы потом достраивали - инженерные войска, по пояс в болотах)

>> Мир меняется.
> просто вы не знаете мир, в котором живете.

меняется-меняется. В древние прекрасные времена рабы назывались "живые убитые". В офис ходить их не заставляли. Правда, жили ровно до праздника сбора урожая. А потом - добро пожаловать воон на ту площадочку. Видите, ржавый меч посередке торчит?

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено СеменСеменыч777 , 11-Апр-21 18:35 
>  всякая ерунда короче ненужная и некачественная

от хозяина зависит.

как известно, Виктор Бут мотает срок в США, там всех припахали собирать какую-то электронику для Томагавков. причем, ни одного из з\к не примут на тот же завод вольным наймом после окончания срока, по соображениям безопасности.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 23:04 
Тонкий передёрг. Смешивание законов общества в одно время, с восприятием и тараканами любого одного индивидуума. Нормально так, зачёт.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Michael Shigorin , 11-Апр-21 21:30 
> Ну а ещё не так давно в мире практиковалось рабство и это
> было традиционно нормальным явлением.

Почитайте про частные тюрьмы в штатах, много для себя узнаете нового насчёт "было".  Хотя и в федеральных там, по словам Бутиной, тоже тот ещё беспредел.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 07:31 
Просто у этих женщин именно "ОН" и был на уме, к тому же слишком хорошее знание ин_юс  до добра не доводит. Русский надо знать - великий и могучий и кок будет соком.
"Инструментарий"
Отправлено Аноним , 10-Апр-21 08:34 
> Сходство звучания Coq и Cock (англ. петух) ...

coq это буквально "петух" с французского, где собственно находится инриа, занимающаяся его разработкой)

"Инструментарий"
Отправлено myhand , 10-Апр-21 19:35 
> где собственно находится инриа

Пойду скажу пацанам, что они в петухе.

PS: Ты русский - освой.  Прям как не-родной...

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 08:54 
У кого что болит.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 09:06 
О доме надо думать.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 09:12 
Я знаю английский, и у меня не ассоциируется со сленговым. Тут дело в характере и воспитании человека. Зачем разработчикам и пользователям этой программы поддавался на издевательски выпады в свою сторону?

Эта ситуация, по-моему даже полезна. Тот кто будет делать издевательские намеки будет записан в разряд быдла. Эффект лакмусовой бумажки выявит всех изнутри гнилых людей.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено тоже Аноним , 10-Апр-21 11:42 
Ой, нашли проблему.
Переписать на питон, обозвать PyCoq - и членовраждующие сразу подавятся аргументами.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 11:57 
PyCoq - а с чем тут будет ассоциация?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено тоже Аноним , 10-Апр-21 12:10 
> PyCoq - а с чем тут будет ассоциация?

Peacock, если хватит фантазии. Если не хватит - ни с чем, что и требовалось.

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Gogi , 10-Апр-21 11:43 
Осталось истеричкам-маразматичкам докопаться до FAQ - десятилетиями существовашее сокращение.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено myhand , 10-Апр-21 13:20 
*****, не подсказывай!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Михрютка , 10-Апр-21 14:17 
назло русским шовинистам переименовать в Habitually Used Inquiries
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 13:11 
Давно пора "одночлены" и "многочлены" выкинуть из цисгендерной шовинистской математики.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 16:35 
Gallina (лат. курица)
Но это оскорбит российских феменисток!
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 16:37 
В СССР^W России феминисток нет
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 16:41 
Когда-то не было.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 07:14 
когда-то были.
А теперь если и есть, то лишь на спецзадании.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 10-Апр-21 16:36 
Ну тогда всем известный проект питон тоже нужно переименовать
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено rvs2016 , 10-Апр-21 19:32 
И сюда инклюзивные добралсь 🤔
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 11-Апр-21 07:15 
а ты я смарю не знаешь что значит это слово?
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено rvs2016 , 11-Апр-21 10:43 
> а ты я смарю не знаешь что значит это слово?

Да опеннета ж начитаешься - и не такого узнаешь! :о)

"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Michael Shigorin , 11-Апр-21 21:17 
На опеннете, кстати, уже родился как-то термин инклюзиция.
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 12-Апр-21 17:54 
Я предпочёл бы не знать ни это слово, ни прочую xepотень, придуманную вами, альтернативно одарёнными, которым некуда себя деть от хорошей жизни
"Инструментарий для доказательства теорем Coq рассматривает в..."
Отправлено Аноним , 13-Апр-21 12:51 
Ну конечно галинабланка или кокос будет лучше. К бабке не ходи!