The OpenNET Project / Index page

[ новости /+++ | форум | wiki | теги | ]



"Инструментарий для доказательства теорем Coq рассматривает возможность смены названия"
Вариант для распечатки  
Пред. тема | След. тема 
Форум Разговоры, обсуждение новостей
Изначальное сообщение [ Отслеживать ]

"Инструментарий для доказательства теорем Coq рассматривает возможность смены названия"  +/
Сообщение от opennews (??), 09-Апр-21, 23:22 
Инструментарий для доказательства теорем Coq рассматривает возможность смены названия. Причина: для англофонов слова "coq" и "cock" (сленговое название мужского полового органа) звучат похоже, и некоторые пользователи-женщины, сталкивались с двусмысленными шутками при использовании названия в устной речи. Само же название языка Coq произошло от фамилии одного из разработчиков, Thierry Coquand. Сходство звучания Coq и Cock (англ. петух) уже обыгрывалось в проекте: язык, используемый для описания конструкций, называется Gallina (лат. курица)...

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

Ответить | Правка | Cообщить модератору

Оглавление

Сообщения [Сортировка по времени | RSS]


1. "Инструментарий для доказательства теорем Coq рассматривает в..."  +9 +/
Сообщение от Hedgehog (??), 09-Апр-21, 23:22 
Зачем эта очень важная "новость" нужна именно на опеннете?
Ответить | Правка | Наверх | Cообщить модератору

6. "Инструментарий для доказательства теорем Coq рассматривает в..."  +24 +/
Сообщение от Антифрактал (?), 09-Апр-21, 23:23 
чтобы ты был в курсе, как мир сходит с ума, подстраиваясь под англицизмы
Ответить | Правка | Наверх | Cообщить модератору

23. "Инструментарий для доказательства теорем Coq рассматривает в..."  +19 +/
Сообщение от Аноним (23), 10-Апр-21, 00:27 
Вернее подстраиваясь под впечатлительных подростков, феминисток, гомосеков и прочих психически неустойчивых личностей
Ответить | Правка | Наверх | Cообщить модератору

82. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (82), 10-Апр-21, 10:01 
анон, ну не смешно вообще. Если ьы он назывался hui - у нас бы точно так же измывались над ним.
Ответить | Правка | Наверх | Cообщить модератору

138. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от RomanCh (ok), 11-Апр-21, 09:50 
Почему "бы"? Пожалуйста: https://gethue.com/

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

Ответить | Правка | Наверх | Cообщить модератору

154. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от ого (?), 11-Апр-21, 19:43 
но истерить до смены названия не стали бы.
Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

161. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Wine_O_Feliya (?), 12-Апр-21, 15:11 
Это как с проектом "pydora"? Где-то в тексте на PyPI можно засвидетельствовать " [..] config file pydora [..]"
Ответить | Правка | К родителю #82 | Наверх | Cообщить модератору

88. "Инструментарий для доказательства теорем Coq рассматривает в..."  +3 +/
Сообщение от Ordu (ok), 10-Апр-21, 10:38 
Обидно, да? Под впечатлительных подростков, феминисток и гомосеков они подстраиваются, а под впечатлительных опеннетовцев, которые до сих пор триггерятся по поводу Pidora они не подстраиваются.
Ответить | Правка | К родителю #23 | Наверх | Cообщить модератору

103. "Инструментарий для доказательства теорем Coq рассматривает в..."  +7 +/
Сообщение от Аноним (23), 10-Апр-21, 13:42 
Так мы просто пошутили и посмеялись, но никто не поднимал серьезно вопрос о переименование.
Этим адекватный человек и отличается от психически больного - тем что тихо хихикает с друзьями, а не выносит подобные вопросы на всеобщее обсуждение.
Ответить | Правка | Наверх | Cообщить модератору

110. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Ordu (ok), 10-Апр-21, 15:04 
А когда людям надоедает это хихиканье "адекватных" и "психически здоровых" при каждом упоминании их проекта, они делают что? Переименовывают проект, чтобы не хихикали.
Ответить | Правка | Наверх | Cообщить модератору

164. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (164), 12-Апр-21, 17:26 
Новость читал? Не автору надоело хихканье, иначе он бы так не назвал. А "некоторые пользователи-женщины" АБИДЕЛИСЬ на "двумысленные шутки".

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

47. "Инструментарий для доказательства теорем Coq рассматривает в..."  +4 +/
Сообщение от Аноним (47), 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

Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

81. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Неа (?), 10-Апр-21, 09:26 
Этот редактор такое же гуано, как и аргументы про Coq
Ответить | Правка | Наверх | Cообщить модератору

83. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Аноним (82), 10-Апр-21, 10:03 
А как тебе ЁбРедактор? Сколько у нас ржали над ё-мобилем? Или это другое? Свое как грица не пахнет?
Ответить | Правка | Наверх | Cообщить модератору

176. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от Noname (??), 13-Апр-21, 15:52 
> ЁбРедактор

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

Ответить | Правка | Наверх | Cообщить модератору

59. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (59), 10-Апр-21, 06:47 
Язык международного общения - английский. Не китайский и не русский как некоторым здесь не хотелось. Если авторы данного инструментария хотят популярности в мировом масштабе, то озаботиться вопросом благозвучного названия естественно.
Ответить | Правка | К родителю #6 | Наверх | Cообщить модератору

63. "Инструментарий для доказательства теорем Coq рассматривает в..."  +14 +/
Сообщение от Тот_Самый_Анонимус (?), 10-Апр-21, 06:56 
>Язык международного общения - английский.

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

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

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

144. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от myhand (ok), 11-Апр-21, 12:15 
Ну, ООН - известна своей научностью.  Там даже Эйлер состоял.

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

Ответить | Правка | Наверх | Cообщить модератору

147. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от RomanCh (ok), 11-Апр-21, 12:44 
> и проч. человеческий мусор.

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


Ответить | Правка | Наверх | Cообщить модератору

84. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от Аноним (82), 10-Апр-21, 10:04 
> этого недоязыка

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

Ответить | Правка | К родителю #63 | Наверх | Cообщить модератору

140. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от RomanCh (ok), 11-Апр-21, 09:57 
> Как грица угадай в какой стране живут нацисты, расисты и шовинисты.

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

145. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от myhand (ok), 11-Апр-21, 12:16 
А зачем с этим что-то делать?  Есть эсперанто.
Ответить | Правка | Наверх | Cообщить модератору

148. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от RomanCh (ok), 11-Апр-21, 12:45 
> А зачем с этим что-то делать?  Есть эсперанто.

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

Ответить | Правка | Наверх | Cообщить модератору

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

занавес

Ответить | Правка | Наверх | Cообщить модератору

166. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Доктор психушки (?), 12-Апр-21, 17:59 
> нацисты, расисты и шовинисты

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

Ответить | Правка | К родителю #84 | Наверх | Cообщить модератору

178. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Noname (??), 13-Апр-21, 15:58 
А что не так?
Ответить | Правка | Наверх | Cообщить модератору

167. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (164), 12-Апр-21, 18:02 
> Как грица угадай в какой стране живут нацисты, расисты и шовинисты.

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

Ответить | Правка | К родителю #84 | Наверх | Cообщить модератору

57. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Аноним (57), 10-Апр-21, 06:02 
> Зачем эта очень важная "новость" нужна именно на опеннете?

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

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

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

Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

127. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (82), 11-Апр-21, 06:57 
"СеменСеменыч777" бы не прошел прежде всего в СССР, ежели бы тот не распался. Потому что уничижительный для Советского человека ник.
Ответить | Правка | Наверх | Cообщить модератору

61. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от myhand (ok), 10-Апр-21, 06:54 
Ну а при каком обстоятельстве посетители opennetу впринципе могли бы узнать, что там не только "негров линчуют", но и формализацией математики занимаются на уровне, за которым уже целым институтам РАН не угнаться?
Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

64. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Тот_Самый_Анонимус (?), 10-Апр-21, 06:59 
>но и формализацией математики занимаются на уровне, за которым уже целым институтам РАН не угнаться?

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

Ответить | Правка | Наверх | Cообщить модератору

66. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от myhand (ok), 10-Апр-21, 07:06 
Ну, представленного общественности инструмента уровня Coq разработано было не было.  Не говоря уже о получении к-л известных формальных доказательств с ним...
Ответить | Правка | Наверх | Cообщить модератору

163. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от НеОН (?), 12-Апр-21, 17:23 
Слава морфу! Слава 404!
Защифрованное послание, которое поймут лишь избранные!
Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

2. "Инструментарий для доказательства теорем Coq рассматривает в..."  +16 +/
Сообщение от Аноним (2), 09-Апр-21, 23:22 
Hey bro nice Coq
Ответить | Правка | Наверх | Cообщить модератору

48. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (-), 10-Апр-21, 02:43 
Nice coq, awesome balls.
terminator.jpg
Ответить | Правка | Наверх | Cообщить модератору

65. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от iPony129412 (?), 10-Апр-21, 07:04 
https://derpicdn.net/img/view/2021/4/2/2584442__safe_artist-...
Ответить | Правка | К родителю #2 | Наверх | Cообщить модератору

80. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Человек под травой (?), 10-Апр-21, 09:25 
Nice coq, swesome proofs.
Ответить | Правка | К родителю #2 | Наверх | Cообщить модератору

162. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Wine_O_Feliya (?), 12-Апр-21, 15:13 
Gallina blank'a bool bool
Ответить | Правка | К родителю #2 | Наверх | Cообщить модератору

3. "Инструментарий для доказательства теорем Coq рассматривает в..."  –4 +/
Сообщение от Аноним (3), 09-Апр-21, 23:22 
Одобряю. Но только если они знали о проблеме с названием, почему назвали язык тоже шуточно - неясно.
Ответить | Правка | Наверх | Cообщить модератору

18. "Инструментарий для доказательства теорем Coq рассматривает в..."  +8 +/
Сообщение от Аноним (18), 09-Апр-21, 23:58 
А они в качестве шутки тогда и сделали такое название. Но то было тогда. а сейчас пришли новые разработчики и настали новые времена, когда не шутят.
Ответить | Правка | Наверх | Cообщить модератору

78. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от пох. (?), 10-Апр-21, 09:21 
Потому что этот Терри совершенно не парится что кто-то на слух воспримет его фамилию как "Петушара". И менять ее не планирует.

Ответить | Правка | Наверх | Cообщить модератору

89. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Тётка с ведром (?), 10-Апр-21, 10:43 
No fun allowed.
Ответить | Правка | К родителю #18 | Наверх | Cообщить модератору

25. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Cradle (?), 10-Апр-21, 00:35 
французы, сэр. Тогда постебались, а теперь боязно стало.
Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

56. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Lex (??), 10-Апр-21, 04:30 
Coq - петух (с франц)
Раньше было модно-молодёжно по дурацки именовать продукт. Не удивлюсь, если те же самые разработчики выросли и внезапно поняли, что это скорее тупо, чем юморнО.
Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

79. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от пох. (?), 10-Апр-21, 09:22 
А фамилию им тоже выросши внезапно сменить? А то ж вызывает нездоровые ассоциации.
Ответить | Правка | Наверх | Cообщить модератору

85. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (82), 10-Апр-21, 10:10 
лол блин. Ты правда считаешь что петух имеет негативную коннотацию во Франции? Петушиная субкультура - она же географически находится в других местах.

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

Ответить | Правка | К родителю #56 | Наверх | Cообщить модератору

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

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

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

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


Ответить | Правка | Наверх | Cообщить модератору

128. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (82), 11-Апр-21, 07:01 
> Вот ты можешь по названию проги - «петух», однозначно догадаться что так называется инструментарий для доказательства теорем ?

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

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

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

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

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

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

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

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

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

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


Ответить | Правка | Наверх | Cообщить модератору

157. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Michael Shigorinemail (ok), 11-Апр-21, 21:25 
> Rar - формат сжатия, разработанный Евгением Рошалом. И название - [Р]ошал [Ар]хиватор.

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

143. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от InuYasha (??), 11-Апр-21, 11:33 
Вообще, FYI, петух во франции - это почти что национальный маскот.
Ответить | Правка | К родителю #85 | Наверх | Cообщить модератору

92. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Gogi (??), 10-Апр-21, 11:39 
Представляю, как сейчас краснеет в гробу Джобс со своим.... ха... ЯБЛОКОМ! :)))
Ответить | Правка | К родителю #56 | Наверх | Cообщить модератору

58. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (57), 10-Апр-21, 06:04 
> - неясно.

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

Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

97. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (97), 10-Апр-21, 12:28 
Потому что в основу Coq положена теория типов "calculus of constructions" (CoC).
Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

4. "Инструментарий для доказательства теорем Coq рассматривает в..."  +7 +/
Сообщение от Аноным (ok), 09-Апр-21, 23:22 
При всем этом остается загадка: как до сих пор не сломлен ГИМП?
Ответить | Правка | Наверх | Cообщить модератору

7. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от Аноним (7), 09-Апр-21, 23:23 
Глимпс
Ответить | Правка | Наверх | Cообщить модератору

17. "Инструментарий для доказательства теорем Coq рассматривает в..."  +5 +/
Сообщение от Стас Михайлов (?), 09-Апр-21, 23:51 
Не существует.
Ответить | Правка | Наверх | Cообщить модератору

74. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (74), 10-Апр-21, 08:51 
Глиномес.
FTGJFIX
Ответить | Правка | К родителю #7 | Наверх | Cообщить модератору

8. "Инструментарий для доказательства теорем Coq рассматривает в..."  +5 +/
Сообщение от Антифрактал (?), 09-Апр-21, 23:24 
Прокудин им не дает сломаться, поит их воткой. Это стимулирует их моск посылать на хрен всех чересчур умных
Ответить | Правка | К родителю #4 | Наверх | Cообщить модератору

10. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Annoynymous (ok), 09-Апр-21, 23:31 
Слава Прокудину!
Ответить | Правка | Наверх | Cообщить модератору

26. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (26), 10-Апр-21, 01:07 
Прокудину слава!
Ответить | Правка | Наверх | Cообщить модератору

41. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (41), 10-Апр-21, 02:01 
Андрей
Ответить | Правка | Наверх | Cообщить модератору

11. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (-), 09-Апр-21, 23:31 
> загадка

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

Ответить | Правка | К родителю #4 | Наверх | Cообщить модератору

19. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноным (ok), 09-Апр-21, 23:59 
Форк же, а не переименован
Ответить | Правка | Наверх | Cообщить модератору

5. "Инструментарий для доказательства теорем Coq рассматривает в..."  +5 +/
Сообщение от Аноним (7), 09-Апр-21, 23:22 
Язык Си - первая буква слова cock.
Ответить | Правка | Наверх | Cообщить модератору

33. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Жорш (?), 10-Апр-21, 01:18 
А rust от ruster - кугут
Ответить | Правка | Наверх | Cообщить модератору

91. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Какаянахренразница (ok), 10-Апр-21, 11:26 
> кугут

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

Ответить | Правка | Наверх | Cообщить модератору

34. "Инструментарий для доказательства теорем Coq рассматривает в..."  +3 +/
Сообщение от Аноним (34), 10-Апр-21, 01:19 
Я прозрел
Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

70. "Инструментарий для доказательства теорем Coq рассматривает в..."  +5 +/
Сообщение от Q2Wemail (?), 10-Апр-21, 08:10 
Думаю, низкосортный вообще и сортирный в частности юмор существовал и раньше.
Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

12. "Инструментарий для доказательства теорем Coq рассматривает в..."  +6 +/
Сообщение от timur.davletshin (ok), 09-Апр-21, 23:32 
Если стеблись, когда называли, то надо продолжать в том же духе. Если у кого-то бомбит, то цель достигнута. Не пойму, почему баб должно от "петушка" бомбить? Я думал, что должно наоборот.
Ответить | Правка | Наверх | Cообщить модератору

21. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (21), 10-Апр-21, 00:10 
Например, можно назвать πdr.
Ответить | Правка | Наверх | Cообщить модератору

27. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (26), 10-Апр-21, 01:10 
> почему баб должно от "петушка" бомбить?

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

Ответить | Правка | К родителю #12 | Наверх | Cообщить модератору

86. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Аноним (82), 10-Апр-21, 10:14 
вообще не врубаешься. Сидят двое коллег пишут доказательства: парень, девушка. Парень подзывает девушку и говорит, показывая на код на экране и глумливо улыбаясь: "Как тебе мой coq?". Я не знаю ни одной даже условно приличной девушки, даже нашей, которая будет долго терпеть такие шутеечки.
Ответить | Правка | Наверх | Cообщить модератору

90. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от n00by (ok), 10-Апр-21, 11:26 
> Я не знаю ни одной даже условно
> приличной девушки, даже нашей, которая будет долго терпеть такие шутеечки.

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

105. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Михрютка (ok), 10-Апр-21, 14:12 
тетка в теме. чтобы сдать лабу - надо отсосать.
Ответить | Правка | Наверх | Cообщить модератору

133. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от n00by (ok), 11-Апр-21, 07:25 
Есть такая штука - шприц для удаления припоя, он же вакуумный оловоотсос, в просторечии "отсосник".  Я с его помощью нерабочий стенд за дипломниками восстановил. За что мне все лабы зачли. ;)
Ответить | Правка | Наверх | Cообщить модератору

129. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (82), 11-Апр-21, 07:04 
Ж))))))
Ответить | Правка | К родителю #90 | Наверх | Cообщить модератору

98. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (98), 10-Апр-21, 12:47 
Анатомию иди отмени. Там не только названия, но и картинки показывают неприличные.
Ответить | Правка | К родителю #86 | Наверх | Cообщить модератору

159. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от пох. (?), 12-Апр-21, 11:03 
уже ж отменили (точнее, пытались): https://kulturomania.ru/news/item/kommunisty-rossii-prizvali.../

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

Ответить | Правка | Наверх | Cообщить модератору

168. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (164), 12-Апр-21, 18:20 
> показывая на код на экране и глумливо улыбаясь: "Как тебе мой coq?"

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

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

Ответить | Правка | К родителю #86 | Наверх | Cообщить модератору

170. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от ого (?), 12-Апр-21, 18:56 
ты бы, конечно, предпочёл, чтобы это были два парня, да?
Ответить | Правка | К родителю #86 | Наверх | Cообщить модератору

45. "Инструментарий для доказательства теорем Coq рассматривает в..."  +4 +/
Сообщение от Аноним (45), 10-Апр-21, 02:23 
Вот же неженки блин, бабу коком напугали. Толи наши люди, ковыряются в Zope молча и не хнычут.  
Ответить | Правка | К родителю #12 | Наверх | Cообщить модератору

87. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (82), 10-Апр-21, 10:15 
Так там же уже Grok или что там?
Ответить | Правка | Наверх | Cообщить модератору

71. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Ag (ok), 10-Апр-21, 08:31 
А представьте когда такие проблемы надо будет разруливать авторам учебников и пособий по птицеводству!
Ответить | Правка | К родителю #12 | Наверх | Cообщить модератору

73. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от timur.davletshin (ok), 10-Апр-21, 08:41 
> А представьте когда такие проблемы надо будет разруливать авторам учебников и пособий
> по птицеводству!

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

Ответить | Правка | Наверх | Cообщить модератору

13. "Инструментарий для доказательства теорем Coq рассматривает в..."  +9 +/
Сообщение от Аноним (13), 09-Апр-21, 23:35 
А еще надо запретить Code Of Conduct
Ответить | Правка | Наверх | Cообщить модератору

36. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Жорш (?), 10-Апр-21, 01:20 
CoC всегда потеха для рубиста
Ответить | Правка | Наверх | Cообщить модератору

15. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (15), 09-Апр-21, 23:41 
Гашина - испанское  слово 😜
Ответить | Правка | Наверх | Cообщить модератору

16. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (16), 09-Апр-21, 23:50 
Так Галина Бланка это не жена Моисея Бланка? Как теперь жить...
Ответить | Правка | Наверх | Cообщить модератору

39. "Инструментарий для доказательства теорем Coq рассматривает в..."  +6 +/
Сообщение от cz (??), 10-Апр-21, 01:52 
На испанском "Gallina blanca" - это вообще "Белая курица". Попробуйте пожить с этим.
Ответить | Правка | Наверх | Cообщить модератору

69. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от n00by (ok), 10-Апр-21, 07:45 
Для Галлов петух тотемная птица, предвестник рассвета.
Ответить | Правка | Наверх | Cообщить модератору

100. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (100), 10-Апр-21, 13:12 
Он для всех нормальных людей предвестник рассвета. Кроме всяких городских озабоченных с подвортами
Ответить | Правка | Наверх | Cообщить модератору

134. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от n00by (ok), 11-Апр-21, 07:46 
Есть версия, что "галлы" и "славяне" -- эдакая лингвистическая калька. Первое родственно с "голос", а второе со "слово". Ныне homo sapiens-ы, а тогда был "человек говорящий".
Ответить | Правка | Наверх | Cообщить модератору

137. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от СеменСеменыч777 (?), 11-Апр-21, 09:04 
> Первое родственно с "голос", а второе со "слово"

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

20. "Инструментарий для доказательства теорем Coq рассматривает в..."  +3 +/
Сообщение от Аноним (18), 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 (по мотивам оригинала). Подойдёт?

Ответить | Правка | Наверх | Cообщить модератору

22. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Дихлофос (?), 10-Апр-21, 00:11 
Предлагаю поменять на Гуч
Ответить | Правка | Наверх | Cообщить модератору

24. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от InuYasha (??), 10-Апр-21, 00:34 
There are no easter eggs in Gallina!
Ответить | Правка | Наверх | Cообщить модератору

29. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Dzen Python (ok), 10-Апр-21, 01:12 
Буль-буль!
Ответить | Правка | Наверх | Cообщить модератору

142. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от InuYasha (??), 11-Апр-21, 11:28 
М-да, у этих анонов нет чувства юмора. )
Ответить | Правка | Наверх | Cообщить модератору

28. "Инструментарий для доказательства теорем Coq рассматривает в..."  –4 +/
Сообщение от Dzen Python (ok), 10-Апр-21, 01:11 
Предлагаю вообще не использовать буквы любого алфавита - они все так или иначе входят в оскорбительные, матерные или эвфеместичные слова, которые оскорбляют книггеров и жирофемок.
Предлагаю вообще не использовать цифры - они тоже могут быть оскорбительны: 14-88 или 13-99 оскорбляют антифа, дни рождения самых страшных маньяков, тиранов, комми и шовинистов состоят из цифр и могут оскорбить любого.
Предлагаю вообще не использовать в названиях спецсимволы - аутисты, дисграфики и клинические слабоумные не могут их ни прочитать, не произнести, а это, между прочим, дискриминация и ущемление.
Ответить | Правка | Наверх | Cообщить модератору

43. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (43), 10-Апр-21, 02:21 
Концу мир!
Ответить | Правка | Наверх | Cообщить модератору

123. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Dzen Python (ok), 10-Апр-21, 19:54 
Да, майн либен?
Ответить | Правка | Наверх | Cообщить модератору

126. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Annoynymous (ok), 11-Апр-21, 01:41 
> Концу мир!

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

Ответить | Правка | К родителю #43 | Наверх | Cообщить модератору

30. "Инструментарий для доказательства теорем Coq рассматривает в..."  +5 +/
Сообщение от Аноним (26), 10-Апр-21, 01:12 
Там это... ВВС не собирается предпринимать срочные меры?
Ответить | Правка | Наверх | Cообщить модератору

31. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от Ingener (??), 10-Апр-21, 01:16 
Да. Правильно. "Кок" это как бы ..лен половой. Надо так назвать - Vagee.
Ответить | Правка | Наверх | Cообщить модератору

32. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (32), 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."
Ответить | Правка | Наверх | Cообщить модератору

35. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (35), 10-Апр-21, 01:20 
А питон этих дам не отпугивает?
Ответить | Правка | Наверх | Cообщить модератору

50. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (50), 10-Апр-21, 03:22 
Многие его не любят, но многие пользуются - на жалость пробивает, вестимо.
Ответить | Правка | Наверх | Cообщить модератору

37. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (37), 10-Апр-21, 01:29 
К чëрту Coq, дамы! Лучше я познакомлю вас со своим Python-ом!
Ответить | Правка | Наверх | Cообщить модератору

38. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (38), 10-Апр-21, 01:49 
твой питончик не идёт ни в какое сравнение с моей анакондой
Ответить | Правка | Наверх | Cообщить модератору

117. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (117), 10-Апр-21, 16:39 
Одноглазой
Ответить | Правка | Наверх | Cообщить модератору

42. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от YetAnotherOnanym (ok), 10-Апр-21, 02:07 
Chick неплохой вариант.
Ответить | Правка | Наверх | Cообщить модератору

46. "Инструментарий для доказательства теорем Coq рассматривает в..."  –2 +/
Сообщение от Аноним (43), 10-Апр-21, 02:23 
Могут перейти на кириллицу и больше не будет проблем.
Ответить | Правка | Наверх | Cообщить модератору

49. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Аноним (49), 10-Апр-21, 03:00 
Вечно эти женщины чем-то недовольны
Ответить | Правка | Наверх | Cообщить модератору

62. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (-), 10-Апр-21, 06:55 
своей внутренней пустотой, видимо
Ответить | Правка | Наверх | Cообщить модератору

119. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Михрютка (ok), 10-Апр-21, 18:11 
а ты заполняй чаще. тогда тебе с утра не только пирожков напекут, но и ядро за тебя сконпелируют, хакер грозный.
Ответить | Правка | Наверх | Cообщить модератору

146. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Annoynymous (ok), 11-Апр-21, 12:17 
> а ты заполняй чаще. тогда тебе с утра не только пирожков напекут,
> но и ядро за тебя сконпелируют, хакер грозный.

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

Ответить | Правка | Наверх | Cообщить модератору

108. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от anonymous (??), 10-Апр-21, 14:57 
Зачем же так прочерчивать линию между мужчинами и женщинами? На самом деле, большинство мужчин и женщин вообще не в курсе про coq.
Ответить | Правка | К родителю #49 | Наверх | Cообщить модератору

51. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (51), 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

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

Ответить | Правка | Наверх | Cообщить модератору

52. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от anonimm (?), 10-Апр-21, 03:58 
Если {an}, n=1,2,... - последовательность, то как политкорректно назвать an?
Ответить | Правка | Наверх | Cообщить модератору

54. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (54), 10-Апр-21, 04:07 
Ну и что?пусть меняют название, от этого мне не холоднее или теплее.
Ответить | Правка | Наверх | Cообщить модератору

60. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от nomad__ (ok), 10-Апр-21, 06:54 
С 80-х годов существует и не было ни у кого проблем с названием. А тут вдруг появились. Бесноватые и сюда добрались.
Ответить | Правка | Наверх | Cообщить модератору

109. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от anonymous (??), 10-Апр-21, 15:00 
Ну а ещё не так давно в мире практиковалось рабство и это было традиционно нормальным явлением. И аналогично "ни у кого не было с этим проблем". Мир меняется. Адаптируйтесь ;)
Ответить | Правка | Наверх | Cообщить модератору

112. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от nomad__ (ok), 10-Апр-21, 15:44 
> Ну а ещё не так давно в мире практиковалось рабство и это
> было традиционно нормальным явлением. И аналогично "ни у кого не было
> с этим проблем". Мир меняется. Адаптируйтесь ;)

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

Ответить | Правка | Наверх | Cообщить модератору

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

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

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

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

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

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

Ответить | Правка | К родителю #109 | Наверх | Cообщить модератору

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

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

Ответить | Правка | Наверх | Cообщить модератору

135. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от СеменСеменыч777 (?), 11-Апр-21, 08:50 
если выражаться политкорректно: философия и этика как её подраздел - это не ваша сильная сторона. просто смиритесь с этим. по мере накопления жизненного опыта может быть что-то и будет.
Ответить | Правка | Наверх | Cообщить модератору

136. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от СеменСеменыч777 (?), 11-Апр-21, 08:58 
если неполиткорректно: какой еще "нашей культуре" ? я отказываюсь иметь общую культуру с SJW всех сортов, хипстреней-смузихлебами и половыми извращенцами.

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

Ответить | Правка | К родителю #130 | Наверх | Cообщить модератору

156. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Michael Shigorinemail (ok), 11-Апр-21, 21:18 
> А вообще отсутствие эмпатии в нашей культуре показывает лишь ее место
> в культуре Человечества

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

Ответить | Правка | К родителю #130 | Наверх | Cообщить модератору

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

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

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

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

Ответить | Правка | К родителю #113 | Наверх | Cообщить модератору

153. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от СеменСеменыч777 (?), 11-Апр-21, 18:35 
>  всякая ерунда короче ненужная и некачественная

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

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

Ответить | Правка | Наверх | Cообщить модератору

125. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (98), 10-Апр-21, 23:04 
Тонкий передёрг. Смешивание законов общества в одно время, с восприятием и тараканами любого одного индивидуума. Нормально так, зачёт.
Ответить | Правка | К родителю #109 | Наверх | Cообщить модератору

158. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Michael Shigorinemail (ok), 11-Апр-21, 21:30 
> Ну а ещё не так давно в мире практиковалось рабство и это
> было традиционно нормальным явлением.

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

Ответить | Правка | К родителю #109 | Наверх | Cообщить модератору

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

72. "Инструментарий"  +1 +/
Сообщение от Аноним (72), 10-Апр-21, 08:34 
> Сходство звучания Coq и Cock (англ. петух) ...

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

Ответить | Правка | Наверх | Cообщить модератору

121. "Инструментарий"  +/
Сообщение от myhand (ok), 10-Апр-21, 19:35 
> где собственно находится инриа

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

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

Ответить | Правка | Наверх | Cообщить модератору

75. "Инструментарий для доказательства теорем Coq рассматривает в..."  –1 +/
Сообщение от Аноним (74), 10-Апр-21, 08:54 
У кого что болит.
Ответить | Правка | Наверх | Cообщить модератору

76. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (76), 10-Апр-21, 09:06 
О доме надо думать.
Ответить | Правка | Наверх | Cообщить модератору

77. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (-), 10-Апр-21, 09:12 
Я знаю английский, и у меня не ассоциируется со сленговым. Тут дело в характере и воспитании человека. Зачем разработчикам и пользователям этой программы поддавался на издевательски выпады в свою сторону?

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

Ответить | Правка | Наверх | Cообщить модератору

93. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от тоже Аноним (ok), 10-Апр-21, 11:42 
Ой, нашли проблему.
Переписать на питон, обозвать PyCoq - и членовраждующие сразу подавятся аргументами.
Ответить | Правка | Наверх | Cообщить модератору

95. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (67), 10-Апр-21, 11:57 
PyCoq - а с чем тут будет ассоциация?
Ответить | Правка | Наверх | Cообщить модератору

96. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от тоже Аноним (ok), 10-Апр-21, 12:10 
> PyCoq - а с чем тут будет ассоциация?

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

Ответить | Правка | Наверх | Cообщить модератору

94. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от Gogi (??), 10-Апр-21, 11:43 
Осталось истеричкам-маразматичкам докопаться до FAQ - десятилетиями существовашее сокращение.
Ответить | Правка | Наверх | Cообщить модератору

101. "Инструментарий для доказательства теорем Coq рассматривает в..."  +2 +/
Сообщение от myhand (ok), 10-Апр-21, 13:20 
*****, не подсказывай!
Ответить | Правка | Наверх | Cообщить модератору

106. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Михрютка (ok), 10-Апр-21, 14:17 
назло русским шовинистам переименовать в Habitually Used Inquiries
Ответить | Правка | К родителю #94 | Наверх | Cообщить модератору

99. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (99), 10-Апр-21, 13:11 
Давно пора "одночлены" и "многочлены" выкинуть из цисгендерной шовинистской математики.
Ответить | Правка | Наверх | Cообщить модератору

114. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (117), 10-Апр-21, 16:35 
Gallina (лат. курица)
Но это оскорбит российских феменисток!
Ответить | Правка | Наверх | Cообщить модератору

116. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (116), 10-Апр-21, 16:37 
В СССР^W России феминисток нет
Ответить | Правка | Наверх | Cообщить модератору

118. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Аноним (117), 10-Апр-21, 16:41 
Когда-то не было.
Ответить | Правка | Наверх | Cообщить модератору

131. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (82), 11-Апр-21, 07:14 
когда-то были.
А теперь если и есть, то лишь на спецзадании.
Ответить | Правка | Наверх | Cообщить модератору

115. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (116), 10-Апр-21, 16:36 
Ну тогда всем известный проект питон тоже нужно переименовать
Ответить | Правка | Наверх | Cообщить модератору

120. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от rvs2016 (ok), 10-Апр-21, 19:32 
И сюда инклюзивные добралсь 🤔
Ответить | Правка | Наверх | Cообщить модератору

132. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (82), 11-Апр-21, 07:15 
а ты я смарю не знаешь что значит это слово?
Ответить | Правка | Наверх | Cообщить модератору

141. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от rvs2016 (ok), 11-Апр-21, 10:43 
> а ты я смарю не знаешь что значит это слово?

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

Ответить | Правка | Наверх | Cообщить модератору

155. "Инструментарий для доказательства теорем Coq рассматривает в..."  +1 +/
Сообщение от Michael Shigorinemail (ok), 11-Апр-21, 21:17 
На опеннете, кстати, уже родился как-то термин инклюзиция.
Ответить | Правка | Наверх | Cообщить модератору

165. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (164), 12-Апр-21, 17:54 
Я предпочёл бы не знать ни это слово, ни прочую xepотень, придуманную вами, альтернативно одарёнными, которым некуда себя деть от хорошей жизни
Ответить | Правка | К родителю #132 | Наверх | Cообщить модератору

173. "Инструментарий для доказательства теорем Coq рассматривает в..."  +/
Сообщение от Аноним (173), 13-Апр-21, 12:51 
Ну конечно галинабланка или кокос будет лучше. К бабке не ходи!
Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема




Спонсоры:
Inferno Solutions
Hosting by Hoster.ru
Хостинг:

Закладки на сайте
Проследить за страницей
Created 1996-2021 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру