Тред успешных хлебателей борщей. Возрождённый.Coq:https://coq.inria.fr/Lean:http://leanprover.github.io/Agda:https://github.com/agda/agdaHoTT:https://github.com/HoTT/HoTThttps://github.com/HoTT/HoTT-Agdahttps://github.com/gebner/hott3По теме: http://groupoid.space/.Cubical Type Theory:https://github.com/mortberg/cubicaltthttps://github.com/mortberg/yacctthttps://github.com/RedPRL/redtthttps://github.com/redprl/sml-redprlhttps://github.com/JetBrains/ArendНу и agda --cubical.По теме: http://cubical.systems/
>>1348837 (OP)Что они делают, автоматически доказывают математические теоремы? Как это выглядит на практике?
>>1348946Они автоматически не доказывают, это уже скорее область всяких https://github.com/FStarLang/FStar и https://github.com/Microsoft/dafny. Но в общем случае доказательство за конечное время сгенерировать нельзя, поэтому даже этим двум надо постоянно подсказывать.Это пруверы же лишь проверяют корректность доказательств. Что, впрочем, очень и очень неплохо.
>>1348946Можно ещё доказывать свойства программ, если язык формализовать https://en.wikipedia.org/wiki/Formal_verification#SoftwareНа практике выглядит как текстовый редактор с "кодом" на особом языке, который строит доказательство определённых утверждений о формальной системе. Можешь глянуть книжку Software Foundations для простого введения.Примеры верификации программ: https://en.wikipedia.org/wiki/Formal_verification#Industry_use
Я какое-то время назад делал свой мета-язык, goviaji. На нем можно определять свой язык программирования, писать на этом новом языке программы, проверять корректность их синтаксиса и типизации, и выполнять их. Все это определяется на простой мета-логической системе (похожей на упрощенный Пролог), а операции выполняются с помощью простого поиска доказательств в глубину. На пиках примеры goviaji-кода.https://github.com/sorrge/goviajiСейчас пересмотрел код свежим взглядом. Во-первых, хотелось бы сделать отдельный пруфчекер, чтобы можно было записывать и проверять отчеты о корректности исполнения. Но самое главное - адски медленно. Для вычисления некоторых простых выражений на Church Numerals требуются минуты. Нотя там всего несколько тысяч шагов в выводе. Унификация, по-видимому, очень медленная. Вот думаю как это улучшить. На кресты можно переделать, там кода мало, будет наверное раз в 1000 быстрее. Но мне нравится Питон, прежде всего его легкая кроссплатформенность. Может, можно как-то радикально улучшить производительность алгоритмически? Я уже запоминаю хеши всех доказанных утверждений, чтобы не доказывать многократно. Но все равно медленно.И хотелось бы комментариев уважаемого борщекоммьюнити по поводу проекта.
>>1348837 (OP)Эх помню были времена гонял конструктивного петушка в самом его логове можно сказать. Тред этот не взлетит, как и прошлый в сущности, инфа соточка. Надо было пилить в math, там бы хотя бы были шансы треду продержаться неограниченное количество времени за счет того что активность там на несколько порядков меньше. Если только конструшок не заглянет на огонек и не разразится немереный срач; но думаю в этот раз не будет этого.Пройдусь немного по пруверам и расскажу разных морозных, может кому-нибудь будет интересно.
>>1349189Отмечу что каждый язычок на перебой соревнуется с другими какую бы похитрожопее систему модулей придумать. fstarСложилось впечатление что проект уже мертв и даже начал разлагаться и пованивать. Неслабо наебался с его установкой. Не помню уже деталей, но дошло даже до того что я под прыщами скачал докер-образ и запускал его из докера. Самая мякотка в том что приложенные примеры выдают ошибки. И я не знаю дело ли в том что они просто забили на эти примеры (что плохо) или еще нужны какие то неведомые настройки которых я не понимаю (что тоже плохо)Очень смешной пример комьюнити в котором жизнь бьет ключомhttps://www.reddit.com/r/fstar/leanОщущения примерно как от fstar, хотя проект поживее наверное за счет того что где то внутри MS некоторая небольшая группка еще подкидывает дровишки, но ставить на него мне совсем не хочется.Тоже долго с ним ебался чтобы завести. Сначала я по собственному недоумению открывал в vscode папку в которой у меня лежит несколько проектов. А оказывается делать этого ни в коем случае нельзя, а надо открывать по принципу одна папка - один проект, чтобы все что нужно автоматически подгрузилось.Хотел побаловаться с проектами xena и mathlib. Вываливается куча ошибок о том что такой-то модуль (на деле практически вообще каждый модуль) использует sorry. Хотя я заглядываю в сорс и вижу что никаким sorry там не пахнет. Следовательно мелкокогении решили таким образом информативно свалить все ошибки в одну корзину. Ну что ж бравО.Самый пиздец - оно ТОРМОЗИТ и ебет процессор вообще не переставая. И жрет дохуищи памяти. Хотя задумка же была написать все на плюсах чтобы летало. Я даже собрал уже проект mathlib. И оно бздело ошибками несколько часов. Но работать быстрее в итоге ничего не стало почему то. Может дело в моей криворукости. Хотя видел комментарии что мол проблемы с производительностью у людей действительно есть.
>>1349192agdaСамый главный подводный камень агды - это конечно же ебаный кусок гнилого кала под названием emacs. Как же у меня бомбит от того что для каждого элементарного действия нужно сыграть целое соло на клавиатуре. Диды во времена телетайпов напридумывали какой то невероятной поебени, поэтому хуй тебе а не адекватные шорткаты вроде ctrl+c ctrl+v которыми пользуется весь мир. Выход по ctrl+c ctrl+x - блядь серьезно? Или ctrl+p ctrl+n для перемещения - я просто хочу чтобы мне как в том кинце с Джимом Керри выжгли тот нейрон в который попала эта информация из самого тупорылого туториала на свете.Хотя я понимаю что у имакса есть свои преданные фанаты. И что их даже не беспокоит гарантированный туннельный синдром. Или что имакс можно настроить вообще совершенно как угодно если только разобраться. Но у меня просто нет вообще никакого желания ебаться еще и с этим в дополнение ко всему прочему.Так же мысль про модули тут особенно актуальна. Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".Прошел несколько глав Стампа. Потом пробовал запустить их же в другом линуксе где стоит версия агды поновее и они нихуя не запускаются. Остается теперь держать старую версию пока не покончу с этой книгой наверное.Еще осилил где то треть лекций макБрайда. Была там забавная история. В конце лекции, которая идет перед лекцией, которая называется чтото типа "комедия непреднамеренных ошибок", он доказывает один кейс и оставляет другой по аналогии. И когда я стал пере-проходить эти упражнения и дошел до этого кейса жестко на нем встал. Для меня стало делом чести его забороть ведь вроде совсем ничего сложного. Тут еще не помогало что в агде то я разбираюсь далеко не так хорошо как хотелось бы. Ну и как то все наложилось. Ебался целый день. Уже блядь выть начал как животное и головой биться. Думал вообще с ума сойду нахуй.А следущую лекцию он начал с того что этот кейс далеко нихуя просто так не доказывается. И все дело в том что там очень важен порядок паттернов при определении функции. Он его поменял и все заработало как часики. Он потом объяснил что к чему подробно. Но честно скажу вот так в голове провернуть какой нужен порядок паттернов в нетривиальных конструкциях чтобы доказывалось все как надо я не смогу. В целом вышел весьма поучительный экспириенс, но и довольно болезненный.
>>1349194coqПока мой самый любимый петушок. Устанавливается за пять секунд, в руке лежит как влитой, быдло очень боится (тест на олдфага). Никаких особых проблем с ним не было. Правда и никаких больших проектов я с ним не пробовал запускать. Только прошел курс SF. Курс btw вообще заебок, в какой то степени изменил мое мироощущение, можно сказать.Поглядывал на NuPRL. Рыскал по сайту полчаса, не меньше. Вроде раньше можно было скачать виртуалку гигов в 20 с ним. А сейчас они вместо этого предлагают использовать их сервера по инвайтам. Короче, отложил я тогда знакомство до лучших времен.
>>1349194>Как же у меня бомбит от того что для каждого элементарного действия нужно сыграть целое соло на клавиатуре. Пользоваться evil религия не позволяет?
>>1349194>Выход по ctrl+c ctrl+x - блядь серьезно?Вообще-то C-x C-c но зачем выходить из имакса, бака?
>>1349194>Или ctrl+p ctrl+n для перемещенияЭто стандартные кнопки для перемещения курсора в консоли Unix. Ты терминалом пользуешься вообще?
Вся суть борщетредов. Расписал стену текста про пруверы, в ответ три камента про то какие кнопки надо нажимать в редакторе. Причем советы, скорее всего, неверные, т.к. комментаторы, очевидно, никогда не пользовались обсуждаемыми программами и даже не знают, для чего они предназначены. Да и сам постер стен текста только запустил примеры и, поглазев на ошибки, удалил.
>>1349130Да. Если совсем на языке тестов, то фишка в том, что такое тестирование позволяет покрыть все случаи.
>>1349247Только те, на которые есть спецификации, и, как правило, лишь с довольно узкой точки зрения корректности результата. Например, спецификация может определять, что результат функции, вычисляющей длину списка, не может быть отрицательным. Если функция не завершается, то обычно верификатор этого не заметит и скажет что все ок. Не говоря уже о том, что вычислительную сложность пока вроде ни один верификатор не осиливает, и реально не работающий из-за конской сложности код пройдет все проверки.
>>1349192>F*Там же вроде только refinement types, не? Оно тогда не совсем прувер.Помню, что у него очень кривой режим для Emacs, который в одном случае выдаст ошибку, а в другом скажет, что всё чекнулось.Ещё помню, что экстракт в F# работает через жопу.>Тоже долго с ним ебался чтобы завести. Сначала я по собственному недоумению открывал в vscode папку в которой у меня лежит несколько проектов. А оказывается делать этого ни в коем случае нельзя, а надо открывать по принципу одна папка - один проект, чтобы все что нужно автоматически подгрузилось.Там совершенно черезжопная система пакетов. Потыкай https://github.com/Kha/elan, может понравится. Но я не тыкал, я ебусь через LEAN_PATH и прочие костыли.>Хотел побаловаться с проектами xena и mathlib. Вываливается куча ошибок о том что такой-то модуль (на деле практически вообще каждый модуль) использует sorry. Хотя я заглядываю в сорс и вижу что никаким sorry там не пахнет. Следовательно мелкокогении решили таким образом информативно свалить все ошибки в одну корзину. Ну что ж бравО.sorry собственно может и не являться им, а быть тактикой admit или незакрытым hole.>Самый пиздец - оно ТОРМОЗИТ и ебет процессор вообще не переставая. И жрет дохуищи памяти.Да, это пиздец, и разработчики не отрицают. Почему писанный на плюсах прувер так тормозит и жрёт память — загадка.
>>1349249>Если функция не завершается, то обычно верификатор этого не заметит и скажет что все ок.Сейчас в каждом втором прувере эвристики проверяют завершимость.
>>1349194>Так же мысль про модули тут особенно актуальна. Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".Там чуть ли ни каждый сделал себе по стандартной библиотеке.Есть вроде как стандартная (https://github.com/agda/agda-stdlib), но нет гарантий, что рандомно взятый туториал будет использовать другую.
>>1349251Эвристиками и корректность можно проверить. Тесты называется. Весь поинт верификации в доказательствах, если их нет то и никакой верификации нет. А их нет.
>>1349231>борщетредов>>1348837 (OP)>хлебателей борщей>>1349132> борщекоммьюнитиА при чем здесь борщ? Помогите знать мемы, чтобы не быть батхертом
>>1349860Если я все правильно понял, это больше для профессиональных математиков тема, а не разработчиков ПО, хотя тут пишут, что можно для улучшения качества тестирования использовать эти штуки.
>>1349250> Почему писанный на плюсах прувер так тормозит и жрёт память — загадка.Как раз таки ничего удивительного, плюсы - это кобол 21 века.
>>1349803Тем, что не нужно двигать предплечье и убирать руки с homerow, а значит можно пользоваться слепой десятипальцевой печатью.
>>1349194>И что их даже не беспокоит гарантированный туннельный синдром. Надвно смотрел серию видосиков по погромированию, где чувак писал в каком-то непопулярном редакторе, и иногда открывал емакс. А в одном видосе он сидел в каких-то ортопедических перчах и тут я заржал знаю, грешно Хороший мем, кароче
>>1349195Еще докину немножкоIdrisК системе как к софту нареканий нет, как минимум чтобы поиграться - устанавливается без проблем, ресурсов как не в себя не жрет. Поддерживаются официально vim и atom. Так что можно как белый человек с ней поиграться. Не помню что там с модулями, но думаю что у Бреди и тут все схвачено.Но как прувер ее использовать это довольно отчаянная затея. Хотя, какие то умельцы перевели часть курса SF на сабж. Помню пробовал поиграться с тактиками и был весьма расстроен. Вроде бы rewrite не поддерживал обратного направления или указания места или еще что. Но это уже все не важно, т.к. тактики теперь депрекейтед и веместо них элаборатор. Думаю, интересная штука, надо бы с ней поиграться.Еще я собрал всю волю в кулак и за 10 часов осилил "Type-driven Development with Idris - Edwin Brady". Но в целом экспириенс вышел так себе. Элементарное ФП я и раньше знал, а вот с более продвинутыми конструкциями вроде коиндукции не уверен что до конца разобрался.Не могу себе представить чтобы я или вообще любой человек не начинающий день с размышлений об устройстве теории типов увидев проблему в виде конечного автомата набросал бы первым делом этот автомат на уровне типов (а не на уровне значений), набросал бы на изичах что то на подобии пикрелейтед и вообще регулярно использовал методологию описанную в книге.
>>1350178IsabelleОтмечу что сам редактор на жабе отжирает гиг памяти при запуске и ML ядро отжирает еще гиг. Вообще систему компактной не назовешь. Но при этом работает все более-менее отзывчиво, прямо летает по сравнению со связкой vscode+lean. Во времена когда чатик может отжирать несколько гигов это наверное пустяки.После петуха такие ощущения, простите уж за странную аналогию, как если после своей уютной и по уму обставленной простенькой квартирки попадаешь в роскошные пестрые хоромы. Вроде бы гораздо бохаче. Но нахуй это все надо - не понятно.Еще у меня полный диссонанс вызвает обилие кавычек расставленных как будто случайно.Думаю надо бы пройти concrete semantics, но все руки не доходят.MetamathА вот это довольно компактненькая системка. Этим она подкупает. И нестандартным подходом к доказательствам через рерайтинг. На сайте у них все как то свалено в кучу. Немного потыкался и так и не придумал куда двигаться дальше.Решил что попробую чтобы набить руку просто повторить все манипуляции из этого видеоhttps://www.youtube.com/watch?v=Rst2hZpWUbUИ я почти добрался до qed, но их горюшко редактор на жабе выбросил эксепшон и был таков. Сил начинать заново у меня уже не было.
>>1350181>MetamathЯ вдохновлялся этой системой при создании goviaji. Автор и его сподвижники немного двинутые на некоторых вещах. Например, основной целью своей деятельности они видят переписывание учебников матана на свою систему, причем в их представлении записи в их системе должны быть максимально похожи на то, что в книгах. Вроде как чтобы студенты могли учить матан по их системе вместно книг. Получается, мягко говоря, не оче, и, естественно, ни один человек в здравом уме не начнет учить матан по их системе и не посоветует это делать другим. Еще мелочи вроде фиксации на сжатом текстовом виде представления доказательств. Изначальный автор вроде был категорически против пруф ассистантов, тактик и тому подобного, все надо было писать руками, так ему казалось более духовно будет. Зацикливались на поиске кратчайших доказательств. Ну кароч сильно своя атмосфера там, хотя люди с виду умные.Самое интересное там для меня это базовая система. Там даже скобки не встроены в синтаксис, система лишь манипулирует последовательностью символов. Скобки определяются как и все остальное, правилами. Но если копнуть поглубже, тоже есть подводные камни, вроде связанных переменных, какой-то системы типов не очень внятного толка. Я уже сейчас не очень помню деталей, но мне не понравилось. Я сделал goviaji на более стандартной и гораздо более понятной базе деревьев и унификации. Если бы можно было выкинуть из их системы эту неочевидную муть, я бы перешел на нее, но она вроде бы необходима и в конечном счете является костылями для ручной реализации унификации.
>>1350252Наверное, тем что математика и доказательство теорем символьной алгеброй (причем, прибитой гвоздями к проприетарному языку и со своими багулями) не ограничивается. Равно как не ограничивается нерадивой школотой, использующей её что бы домашку аналитически с выкладками порешать, чтобы училка одобряе и ленивыми инженеграми, использующими символьную алгебру для того же.
>>1350296Нет. Как и нет доказательства корректности реализации чего бы то ни было еще. Так если подумать, вообще никаких доказательств нет. Что могут доказать лысые обезьяны с помощью своих животных звуков?Увы, мы можем лишь уповать на то, что в более простой программе меньше вероятность ошибок. Вот, например, в metamath ядро парсера и пруфчекера довольно маленькое и, что важно, простое. Но, на мой взгляд, не настолько простое, как могло бы быть, хотя тут уже возможны разные мнения: простоту трудно точно определить. goviaji это попытка сделать по-другому, по возможности еще проще.С этой т.з. другие пруверы проигрывают: там в качестве базовой логики выбирается, как правило, очень богатая система, с кучей правил (еще попробуй найди точное определение), каких-то тонких моментов (авторы обычно их замалчивают для ясности - чего людей техническими деталями пугать?), и довольно трудной и запутанной реализацией.
>>1350336Да, конечно, он самый.Единственный его недостаток, на мой взгляд, это то что уж больно там дохуя всего. Проходил я его ну очень долго, в основном из-за собственного распиздяйства, не буду даже писать сколько чтобы никого не пугать. Пока дошел до середины, зашел глянуть на их сайт, они все переворошили и несколько глав добавили. Когда я проходил было около 40 глав. Вообще я считаю что совершенство - это когда нечего убрать. Но они придерживаются похоже противоположной философии и курс постоянно разрастается как раковая опухоль. Уже на четыре книги разбили.Еще есть похожий (но явно покороче) курс от Вадлера на агде:https://plfa.github.io/
>>1350427> не буду даже писать сколько чтобы никого не пугатьПосле того, как я на SICP потратил год с хуем, меня уже ничего не напугает.
Пересматривая код, внезапно нашел еще одну проблему в своей реализации простых языков на goviaji. Если рассмотреть термыlambda x. ylambda x. falseто с т.з. простого синтаксического анализа y и false это одна и та же категория, т.е. у меня это "переменные". На самом деле false может быть константой языка, для него могут быть определены какие-то правила, а может и не быть. Но, например, предикат для определения свободных переменных в терме никак не сможет узнать, есть ли что-нибудь особенное у false или нет. В моем коде false всегда будет считаться переменной. Сейчас там все работает и так, но реально внутри программы полная чушь происходит из-за этого. В metamath сделали типы "переменная" и "константа", и заставляют пользователя определять тип для каждого используемого имени.Альтернативно, можно всегда переменные оборачивать в специальный функтор, например:lambda (var x). (var y)или делать это специальным префиксом, как в пхп каком-нибудь. Но по сути это то же самое, разве что локальный синтаксис.Сейчас у меня есть список того, что не может быть переменной, туда всякие ключевые слова занесены. Можно в этот список внести все константы. Проблема в том, что этот список принципиально нельзя расширить: он определяется один раз, одним предикатом. Это из-за того, что в моей монотонной металогике добавлением новых правил нельзя сделать ложными какие-то утверждения, которые были истинными до этого. Например, если variable false было истинным, то оно всегда останется истинным, какие правила ни добавляй.А это значит, что нельзя по-простому расширить язык, добавив новые правила. Например, я (неправильно) расширял лямбда-исчисление типом bool и конструкцией if-then-else, добавив правила для нового синтаксиса и семантики. По идее нужно сделать так, чтобы bool, true, false, if, then, else больше не считались переменными. Но это невозможно из-за монотонности. Получается, что определение языка не может быть полностью реюзабельным: по крайней мере список констант придется каждый раз декларировать заново. Мне от этого неуютно.
>>1349194>Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".Ну здраститя. Их аж две - agda-prelude https://github.com/UlfNorell/agda-prelude и standard-library https://github.com/agda/agda-stdlib и даже три, еще iowa agda library, но установка несколько аутичная с неочевидными моментами (мне даже Норелла пришлось трясти на предмет почему его поделие (prelude) ошибки выдает, оказалось, для агды 2.5.4.2 нужно использовать бранч 2.5.4.2-compat). Как по мне, в агде и идрисе интереснее всего т.н. "дыры", в коке чего-то такого очень не хватает.>Самый главный подводный камень агды - это конечно же ебаный кусок гнилого кала под названием emacsНу она и без емакса работает, в атоме. Но клавиатурные комбинации там те же, так что формально - обмен шила на мыло. >Пока мой самый любимый петушок. Устанавливается за пять секунд, в руке лежит как влитой, быдло очень боитсяКок в виде установщика под винду малополезен, хотя там с ним и ставится полторы либы. Вся петушиная сила доступна только под линуксом, где можно и стандартные либы ставить и конпелять нестандартные.
>>1350316>Нет. Как и нет доказательства корректности реализации чего бы то ни было еще. Так если подумать, вообще никаких доказательств нет. Что могут доказать лысые обезьяны с помощью своих животных звуков?Нафига тогда тебе вообще пруверы, если конструктивизм, на котором все они основаны, начинается с признания математики подмножеством животных звуков лысых обезьян? Без антиплатонизма в этой теме вообще делать нечего.
>>1350606Ну все верно. y и false - свободные переменные. Хочешь, чтобы они стали связанными - пили окружение, или абстрагируйся.
Посоны, как сделать, чтобы Coq экстрактил в тупль из прелюдии, а не создавал data Prod a b = Pair a b?
>>1350875Мне нужно сделать так, чтобы некоторые имена не были свободными переменными. Связать их тоже не с чем, это должна быть константа сама по себе, определенная с помощью правил вывода, напримерeval (if false then T2 else T3) T3То есть все отличие false от y в том, что для false есть такие правила, а для y нет. Ну и это не работает, вот.>или абстрагируйсяВот этого не понял.Вообще я уже придумал, как это решить с помощью derived forms. Все константы заменяются на термы с маркером, что это константа:false = (constant c_false)Тогда константы легко отличить от переменных, не зная конкретных имен. Так же и с ключевыми словами вроде if. Теперь расширения языка можно делать, добавляя новые derived forms и правила. В выражение lambda x. false в чистом лямбда-исчислении false будет переменной. А если доопределить язык булами, то оно будет преобразовано в lambda x. (constant c_false) и будет иметь другую семантику, как лямбда всегда возвращающая константу false.
>>1350835>Их аж две .. и даже триПолучается они не такие уж стандартные>но установка несколько аутичнаяО чем и речь.По поводу атома - не понимаю как я мог его пропустить. Возможно, что когда я смотрел, примерно год назад, там не было полной функциональности вроде кейс-сплита. Или даже более вероятно, что перебирая разные сочетания пруверов и редакторов я просто проскочил этот вариант. Но, спасибо за наводку.>Но клавиатурные комбинации там те жеДа имхо лучше бы было хотя бы ctrl+alt+X как в идрисе-атоме.>Кок в виде установщика под винду малополезен, хотя там с ним и ставится полторы либы. Вся петушиная сила доступна только под линуксом, где можно и стандартные либы ставить и конпелять нестандартные. По мне так сложности возникающие под виндой весьма преувеличены. В основном они возникают когда требуется запустить нечто слепленное из говна и палок баш скриптами или заточенной под какую то чисто линуксовую функциональность. И от того что разрабы совершенно кладут на винду хуй, конечно же.Вот например установка агды под винду это еще тот цирк. Можно либо через кабал установить, либо инсталлером. Я конечно же не ищу легких путей и попробовал оба варианта и могу сказать что они оба в принципе работают. Для меня только великая загадка почему разрабы сделали инсталятор все-в-одном с хаскелл-платформой и всем-всем-всем, но не сделали отдельный блядь инсталятор агды под винду т.е. такой в котором были бы только нужные бинарники. Я "в ручную" извлек с помощью msi-экстрактора нужные файлы из их огромного инсталятора и получил вроде бы работоспособный вариант.Правда в итоге возник затык в самом неожиданном месте - со шрифтами. И я плюнув на все запустил бубнту в виртуалке.
>>1351150Я тут отхожу от темы треда, но уже не могу остановиться. Современное положение с установкой софта вообще никуда не годится. Совершенно неприемлемо что любая программка может писать и читать вообще куда угодно на диске и размазывается тонким слоем по всей системе.Так же меня весьма раздражают дот-файлы. Очень порадовал недавний пост на реддите, а то я реально думал что я один такой у кого люто бомбит со всей это точечковой хуиты.https://www.reddit.com/r/programming/comments/amp06h/dotfile_madness/
>>1351170Но я ведь не пидор.К тому же традиция дристать дот-файлами идет явно из юникс-вея и для макбучных хипстерков тоже является нормой.
>>1351661>К тому же традиция дристать дот-файлами идет явно из юникс-вея Щито ты несешь. XDG_xxx давным-давно есть. То что криворукие нехорошие девелоперы кладут на это хуй и хуячат куда попало - это проблема криворуких нехороших девелоперов.>любая программка может писать и читать вообще куда угодно на дискеНе может.
>>13517041 Идея здравая, более чем. Реализовано все через сраку, как обычно.>LibreOffice Windows x64 MSI: 238 MB>LibreOffice snap: 1.1 GBНо может еще получше сделают>Snappy Is Finally Doing Something About Super Large App Sizes2. Нет не заебусь. Чистейший фад.>>1351707>XDG_xxxТолько всем насрать.>Не может.Нет, может. Ты наверняка намекаешь на модель "безопасности" которой прыщеглазики так гордятся. Эта модель чистейшей воды безумный манямирок и профанация. См. пикрелейтед.Ну ты можешь радоваться что программа спрашивает у тебя разрешения чтобы раздристаться по диску. Ты можешь его не давать и не устанавливать программу. Такая то швабодка.
>>1351150> Вот например установка агды под винду это еще тот цирк. Можно либо через кабал установить, либо инсталлером.Через stack все ставится в одну команду. Главное, чтобы учетка винды была без русских букв. В инсталлере старая версия, а кабал вообще для наркоманов. Но да, Идрис вот на винде правильно сделали, распаковываешь архив и все сразу работает. > По мне так сложности возникающие под виндой весьма преувеличены. В основном они возникают когда требуется запустить нечто слепленное из говна и палок баш скриптами или заточенной под какую то чисто линуксовую функциональность. Ну и как из виндовского установщика кока поставить хотя бы либы из opam репозитория? В бубунте opam install vst и вуаля, а как тот же vst в винде накатить?
>>1350934>Мне нужно сделать так, чтобы некоторые имена не были свободными переменными.Это достигается созданием окружения, например, где-то в division в коболе, лол описываешь все возможные константы языка. Либо твоим способом с синтаксической заменой, но в твоем способе нельзя использовать constant как часть языка.
А вот в goviaji прувер бы запомнил, что ОП не Сохацкий, и не доказывал бы больше одного раза.Кстати, на тему корректности реализации: отладил неочевидный баг в прувере недавно, который раньше не проявлялся. Наверное, там еще есть.
Агда интересна ещё тем, что в следующем релизе (а в нынешней девелопмент версии уже есть) будет cubicaltt искаропки. В кок, Идрис и остальные пруверы это завозить вроде пока вообще не собираются (?).
>>1352593говно для академиков, не обращай внимания. в проде здоровые люди это использовать никогда не будут
>>1352595> в проде здоровые люди это использовать никогда не будутБудут. Лет через 30. Не как отдельный прувер, конечно, а как фичу продакшн- быдлоязыка типа той же джябы или что там будет в моде.
>>1352615и через тридцать лет не будут. нахуй не нужна корректность, нужно фичи пилить - быстро, дёшево, и чтобы хоть как-то работало
>>1352618>нахуй не нужны ваши циклы и функции, нужно фичи пилить, чтобы хоть как-то работало>нахуй не нужна ваша портабельность, нужно фичи пилить, чтобы хотя бы как-то на той же системе работало>нахуй не нужен ваш сборщик мусора, нужно фичи пилить, чтобы быстро и хоть как-то работало>нахуй не нужны ваши модули, текстовых инклюдов хватит всем и вообще нужно фичи пилить, чтобы хоть как-то работало>нахуй не нужны ваши лямбды, нужно форичи пилить, чтобы хоть как-то работало>нахуй не нужны ваши тайпклассы, нужно фичи пилить, чтобы хоть как-то одним классом реализовать интерфейс и все как-то работало>нахуй не нужна ваша иммутабельность, нужно фичи пилить, чтобы на одном ядре хоть как-то работало>нахуй не нужны ваши монады, нужно фичи пилить, чтобы копипастить код и рассказывать на собесах про паттерны и чтобы хоть как-то работало...>нахуй не нужна корректность, нужно фичи пилить - быстро, дёшево, и чтобы хоть как-то работало
>>1352693всё что нужно - это циклы, функции, простые структуры данных + что-то реально полезное, как например в го сделано. поэтому он и популярен. хотя смысл расписывать "элитарию" вообще, ему же шашечки нужны, а не ехать
>>1352766> всё что нужно - это циклы, функции, простые структуры данных + что-то реально полезноеТ.е, кроме С вообще ничего не нужно, я тебя понял. Однако, куча всего есть и активно используется в продакшене. Я к чему, даже не сомневайся, что на яп с корректностью, тактиками, автозаполнениями дыр итд, хипстеры налетят только в путь. Ещё и наперебой орать будут "ебаный бабай, как жи мы без всего этого раньше жили?!". Дело только в том, чтобы сделать все это доступным любой макаке с соевыми мозгами. Тот же Идрис нихуя не для широких масс и уж тем более не для продакшена, хуй там даже хеловорлд напишешь и поймешь написанное без минимальных познаний в теории типов.
Мдауш, в любом треде про пруверы от половины постов - про Сохацкого. Знатно он дегродам дупы разворотил, долго его ещё анальные погорельцы помнить будут.
>>1353610>Знатно он дегродам дупы разворотил, долго его ещё анальные погорельцы помнить будут. А что было то, напомни?
Единственная проблема с пруверами - никто не знает теорию типов достаточно для того, чтобы придумать ей хоть какое-то практическое применение. Всякая быдлота уровня местных тыжпрограммистов максимум на что способна в плане теории типов - гореть от Сохацкого, который на них ссать не хотел. Какие-то практические идеи даже обсудить не с кем. Вы хоть сами осознаете, какое вы дно?
>>1354578Тебе никто ничего не собирается доказывать, научись думать своей головой и не строй обиженку.
>>1354578>придумать ей хоть какое-то практическое применениеА зачем ей практическое применение? Или это специфика /pr?>гореть от СохацкогоЗачем обращать на него внимание? Вся его активность в теории типов -- создание собственного бренда. Ничего полезного он не сделал.>Какие-то практические идеи даже обсудить не с кем.А что ты можешь предложить, кроме оскорблений?
>>1355082> Тебе никто ничего не собирается доказывать,А где я прошу мне что-то доказать? Я просто факты констатирую.>>1355097> А зачем ей практическое применение? Затем что вычислительные теории типов - MLTT, UTT итд для этого и создавались. Вон, Брэди для Идриса целую парадигму программирования придумал, type-driven development. Чтобы это использовать, даже познаний особых в теории типов не нужно, хватит примеров из самой книжки. Нет, не хотим. Хотим с сохацького гореть. > Вся его активность в теории типов -- создание собственного бренда. Ничего полезного он не сделал.Ну он не Барендрегт или Мартин-Леф, чтобы что-то выдающееся сделать в теории типов. Но с точки зрения практической реализации чисто теоретических идей он сделал побольше, чем любой другой житель СНГ, это факт. В расеюшке вообще никто прувер сделать не в состоянии.
>>1355523>Затем что вычислительные теории типов - MLTT, UTT итд для этого и создавались.Мм, вообще-то нет. Не было в мыслях у Мартин-Лефа, что на компьютерах будут ПО верифицировать. Практические применения для математиков /= практические применения разработчиков, что, как мне кажется, ты имеешь ввиду упоминая Брэди. Это только последние 20-30 лет type theory пытаются использовать для software verification, а раньше это было про математику и логику. Даже сейчас пруверы на основе HoTT в первую очередь создаются в контексте оснований математики, а не для факториалов. Практически ориентированный только Idris.>Но с точки зрения практической реализации чисто теоретических идей он сделал побольше, чем любой другой житель СНГ, это факт.Это лишь говорит о твоей малой осведомленности в теме и подтверждает, что Сохацкий в первую очередь громче всех о себе кричит.>В расеюшке вообще никто прувер сделать не в состоянии.Ну что за глупости. Ты бы хоть в шапку посмотрел, заметил Arend. Валерий Исаев в отличии от Сохацкого занят делом и пишет папиры и пруверы, а не строчит в твиттер о своей охуенности и не создает сайты с лендингами.И поверь, есть другие люди, способные создавать пруверы, просто они заняты своим делом.
>>1355523>А где я прошу мне что-то доказать? Если ты не понял мысль в посте, я объяснять ее не буду. Твой бред начинает надоедать.
>>1355562>в отличии от Сохацкого занят деломСильное утверждение. Проверять его на соответствие действительности мы, конечно, не будем.
Нейрончиков тред перекатывать не хочете, возобновили вновь старую тенденцию с пруверами. Не кажется ли вам, что всё это устарело уже? Нужен новый подход.
>>1352586>Он и как "хуяк-хяук" - говно полное.>Лучше сразу Coq взять и в Haskell его экстрактить.Как на Coq хуяк-хуяк сделать partial функцию или не примитивно рекурсивную? E.g. head или mergesort. Так чтобы не сойти с ума в процессе.
>>1353846Так что там за история, кто-нибудь?Это не он пилил прувер на эрланге? Немного я припустил подливы с этого выбора языка.
>>1355859> сделать partial функцию А зачем тебе верификация, если ты partial функции хуячишь? > или не примитивно рекурсивнуюСам бы хотел знать, с радостью готов быть обоссаным Coq-боярами.
Беда всех этих языков это инфраструктура, решил было туториал по агде пройти, полдня прикручивал ее к виму, получилось хуево, бросил эту затею. А Coq вообще себе на уме, хоть и установить легко, после хачкелля вообще не идет. И, конечно, я не могу представить себе математика в здравом уме, ебущимся с кейбандами, емакса, зависимостями, совместимостями версий, фп- заморочками и прочим, чтобы велосипедить целые теории, в надежде дойти хоть до результатов 60х годов. Энтузиазм выше крыши нужен.
>>1355562>Валерий Исаев в отличии от Сохацкого занят деломоднокурсник твой? Единственный человек из СНГ который что-то сделал для теории типов поехал крышей и умер 2 года назад, а остальное исаевы акуклевы какие-то ебланы-программисты, статей много, а импакта никакого.
>>1356050> Беда всех этих языков это инфраструктура, решил было туториал по агде пройти, полдня прикручивал ее к виму,Это твоя беда. Агда к емаксу прикручивается одной командой а к атому - несколькими кликами мышкой. Мартин-Леф тебе чтоли виноват, что ты не можешь даже установить то, чем собрался пользоваться?
В чем вообще заключается это прикручивание? Это же просто редакторы. Что вам там надо-то? Автодополнение? РЕПЛ какой-то продвинутый? Зачем?
>>1356089> В чем вообще заключается это прикручивание? Это же просто редакторы. Что вам там надо-то?В случае агды без редактора вообще можно только компилировать, интерактивного взаимодействия с голой агдой не существует. А там вся философия во взаимодействии пользователя с агдой через последовательно усложняющуюся типизацию и дыры. Ну ещё некое подобие тактик есть. Для всего этого нужен редактор. В идрисе изначально репл есть, но опять-таки что-то посложнее сделать - нужен редактор, у того же Брэди все примеры с атомом.
>>1356088>говно сумасшедшего поедателя мозолек на диалекте лиспа>говно на электроне выжирающее все память на стартеНет, спасибо, все что начинается с "установите емакс" должно лежать под землей, как достояние узкого кружка сумасшедших. И еще удивляются, чей-то их язык непопулярен.
>>1356192> И еще удивляются, чей-то их язык непопулярен.С больной головы на здоровую. Кок без емакса и атома работает и существует 30+ лет и что, дохуя он популярен? Проблема в вас.
>>1350199>>1350181>>1350178>>1349195>>1349194>>1349192А вот эту хрень видел? https://try.imandra.ai/Стал ReasonML учить -- всплывала в реддите несколько раз.
>>1356244> As a programming language, Imandra is a subset of the functional language OCaml. We call this subset of OCaml Обрезанный окамл с нескучными обоями. Уноси.
>>1356192> как достояние узкого кружка сумасшедшихНу так сами пруверы - это достояние узкого кружка сумасшедших. Не для ерохиных тема.
>>1356328Ну так приходят математики: слишком сложна, уходят набирать "очевидно" в latex. Приходят программисты: сложна, уходят писать идрисы свои.
>>1355862Да при чем тут эрланг, ноль информации в твоих каментах.Такое ощущение что ты перед кем-то выйобуешься.Передо мной не нужно, для меня ты никто.
>>1356196>Кок без емакса и атома работает и существует 30+ лет и чтоОтмечу что при этом не более чем год назад появилась в coqide убойная фича - при переносе строки учитываются табы на предыдущей строке - доступная чуть ли не в любом редакторе размером от нескольких килобайт. Такими темпами они выйдут на паритет по функциональности с такими редакторами как sublime или vscode (или черт его дери emacs) лет через сто.
>>1356244Если уж к поделкам MS я отношусь со скепсисом, то к этому поделию непонятной мутной конторки, вполне возможно состоящей из единственного хипстерка - почти как к червю пидору. Возможно я ошибаюсь, из нескольких минут наблюдений1) один пост на реддите в r/imandra - переплюнули fstar2) НЕТ СОРЦОВ?3) вместо установщика - говно из курлпайпа плюс несколько часов компиляний4) не работает под шиндовсГлавное - как и с большинством васяноподелок языков, регулярно всплывающих раз месяц с нескучными заимствованиями разных синтаксических конструкций, непонятно нахуя вообще нужно это чудо, для чего? В чем его фишка?
>>1356034>А зачем тебе верификация, если ты partial функции хуячишь?прост))))) Можно например в месте вызова аргументы проверять чтобы не терять корректность. В агде вроде бы даже можно код с дырками запускать, правда не знаю на сколько это на практике полезно и что будет если такой код экстрактить.
>>1356377> Отмечу что при этом не более чем год назад появилась в coqide убойная фича - при переносе строки учитываются табы на предыдущей строке - доступная чуть ли не в любом редакторе размером от нескольких килобайт.А это очень нужно для коковского кода?
>>1352766Го популярен из-за того, что у него няшный логотип и его пиарит гугл. Все. Его, кстати, переписывают (привет слоупокам) ломая обратную совместимость, и во второй версии добавляют и дженерики, и обработку ошибок, и все остальное, о чем Пайку талдычили с самого начала.Алсо, сборщик мусора и модули - это "шашечки", я тебя услышал. Иди дальше laba1.cpp дописывай.>>1356762Нужен, ибо без нормальной реализации персистентных структур в наше время никуда rc - это один из вариантов gc, напоминаю.
>>1356569>А это очень нужно для коковского кода? Ну как бы да - не все же ебошут все в одну строчку. Хотя и такие черти бывают, чего уж там.Вообще интересно почему так - код надо хитровыебно выравнивать, а с обычным текстом никто так никогда не делает.
>>1356773>Его, кстати, переписывают (привет слоупокам)>и во второй версии добавляют и дженерики, и обработку ошибок, и все остальное, о чем Пайку талдычили с самого начала.Врети! Линк?>ломая обратную совместимостьБудет обсер гарантия миллион процентов. Гарантирую тот же исход хипстерков с ангуляра на реакт 2.0 - т.е. с го на еще какую нибудь новомодную поебень. Может даже typescript. Или еще чего придумают новенького.
>>1356762>С линейными и uniqueness типамиКакое положение этих штук с точки зрения зависимых типов, доказательств и прочего Карри-Ховарда?Какое место эти типы занимают на лямбда-кубе?
>>1357001>Какое место эти типы занимают на лямбда-кубе?Любое. Зависит от того, как calculus построишь.В лямбда-кубе три плоскости, а substructural типы это совсем другая плоскость. То есть, ты выбираешь любую точку на лямбда кубе - это какое-то семейство исчислений, и уже его расширяешь линейными, аффинными, whatever типами.>Какое положение этих штук с точки зрения зависимых типов, доказательств и прочего Карри-Ховарда?Ортогональное. Это тоже про доказательства, но в другую сторону. А как оно все вместе взаимодействует - предмет bleeding edge research последних минимум лет двадцати.
>>1357030Так ведь хохма этого куба в том что местные петухи его притаскивают чтобы всем доказать что депендент-калькулус самая-самая вершина эволюции и выше его уже ничего не может быть. А тут вона оно как получается.А как, кстати, новомодные кубические типы сочетаются с линейными, кто-нибудь брался за такое?
>>1357000>Врети! Линк?https://github.com/golang/go/wiki/Go2 не?>новомодную поебень>typescriptНу такое.У гугла кстати то же самое ведь уже было с дартом, один в один. Только там язык еще хуевее го был, ну то есть вообще кроме нескучных обоев от гугла ничего не было. Некоторые хипстерки заглотили, через некоторое время стало понятно, что он нихуя не взлетел, ну гугель их и кинул, потом вот вторую версию точно также выкатили, все попутно сломав, ну и опять маховик маркетинговой машины разгоняют. Переписывай код своего стартапа, хипстерок, код сам себя не перепишет.
>>1357515> Так ведь хохма этого куба в том что местные петухи его притаскивают чтобы всем доказать что депендент-калькулус самая-самая вершина эволюции и выше его уже ничего не может быть. А тут вона оно как получается.Че получается-то, мань? Ты хоть разберись в вопросе, потом называй петухом кого-то кроме отражения в зеркале. Самая упакованная вершина куба это СоС, calculus of construction. CIC - исчисление индуктивных построений, на чем основан тот же кок, уже выше. А зависимые типы начинаются вообще с лямбды пи. Этот куб вообще касается только лямбда исчислений по Черчу, лямбды а-ля Карри к нему вообще не относятся. И так далее. Двоечка тебе, уроки иди делай.
>>1357549О а вот и порваный петух прилетел. Ну я рад что ты все таки разобрался что там к чему, может теперь поменьше будешь насаться с этим кубом как с писаной торбой>Двоечка тебе, уроки иди делай.Сначала сдай норматив чтобы тут указания раздавать. Первый вопрос норматива>Перечислить все аксиомы CICвремя пошло.
>>1357530>ломая обратную совместимость>We do not want to break the ecosystem. Go 1 and Go 2 code must be able to interoperate in programs with ease.Что то тут не сходится
>>1357708Долбаеб, блядь. О чем говорить с дегродом, который не отличает лямбда исчислений от вспомогательных построений на их основе.
>>1357715>Go 1 and Go 2 code must be able to interoperate in programs with ease.Подумай еще раз.>>1357716Назвать тайпскрипт новомодным язык не поворачивается. Он же и не новый, и не модный.
Представьте себе пространство всех языков программирования — понятно дело все знают про лямбда исчисление. Но не многие же рубисты или ПХП программисты задумываются, что они пишут на языке пространства — которое с точностью до битов моделируется теорией типов Мартина Лефа (надо только вселенные правильно отконфигурировать, это научились делать в 2001 году, когда Coq все дружно писали). Конечно я сам в это по началу не верил, и думал что есть все-таки ограничения и что Данила Мастер, который вручную все сам делает вместо того чтобы экстрактить это из Инфинити Топоса делает ненапрасный труд. Мне пришлось написать прувер чтобы понять — таки да, каждый Данила Мастер, который считает себя инженером — производит временный и бесполезный труд, давая ярлыки феноменам не видя их сути.Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы. Так как изоморфных типов в пространстве бесконечного топоса хватает, то в MLTT тоже есть что-то похожее на матрицу гомотопических групп. Они имеют разные имена и могут в принципе не проходить чеканье на равенство и т.д., но при компиляции в нетимизированную лямбду изоморфные типы будут генерировать совместимый код.У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.
Ясно, этот >>1358311 опущ прохудился, замените по гарантии. >>1358313Охуенная паста, никто кроме Сохацкого так не напишет.
>>1358475Вообщем если есть вопросы я отвечу, высмеяли меня хорошо, я люблю анонимусов они дают взгляд на себя долбоеба со стороны!
>>1358615> Говно без задач, не нужное ни программистам, ни математикам. Вторая культура и там и тут.MLTT это самая что ни на есть первая культура, основания. Не нужна она только дегенератам, для программистов и математиков польза есть, дело в том что средний пидор в узкачах с поворотами, с бородкой и петушиным гребнем из барбишопа - это не программист и не математик, а простое быдло.
>>1358309Держи в курсе, только делай это в другом треде. >>1358313У меня от этой пасты кровь приливает к мандале и сразу хочется преподавать математику 11-летним детям, все правильно?
>>1358712>Держи в курсе, только делай это в другом треде. Лучше уж ты предупреждай когда снова соберешься запиздеться, чтобы время на твои охуительные истории не тратить.>У меня от этой пасты кровь приливает к мандале и сразу хочется преподавать математику 11-летним детям, все правильно?Главное чтобы к кое чему другому не приливало, а так норм.
>>1358387>опущ прохудился>Ни слова про нормативНет, маня, прохудилась тут только ты.Где ответы на норматив? Часики то тикают.
Кто-нибудь может пояснить чем занимался Воеводский и ко?Я так понял они хотели создать основания для математики такие что их принимало бы большинство математиков, типа в них можно было бы выстраивать эти ваши ебалогии. И так же удобные для работы на компьютере.Но я вижу только два артефакта их деятельности. Первый - библиотека на коке/агде. Для чего она вообще нужна мне не понятно. Она кем-нибудь используется вообще? Второе - конференции. Устроены они по принципу - каждый желающий приходит и рассказывает свои охуительные истории хотя бы по касательной касающиеся темы оснований. Как то все совсем мутно.
>>1359005Бля, вот только что зашёл в тред первый раз, начал читать и думаю интересно, взлетела ли та хуита, которую Воеводский мутил и тут твой пост. Вот как это объяснить? Может я ебанулся и подменил себе воспоминания, а твой пост был раньше? Или это просто мир волнами информационными хуячит и мы на одной волне зашли? А?
>>1359005> Кто-нибудь может пояснить чем занимался Воеводский и ко?В двух словах - конструктивные основания. > - библиотека на коке/агде. Для чего она вообще нужна мне не понятно. Она кем-нибудь используется вообще?Попытка реализации конструктивных оснований. Она никем не используется, потому что в MLTT могут единицы, в её дальнейшее развитие - HoTT могут ещё меньше, а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкий. Так и живём, сладкий хлеб жуем. Ибо папуасы.
>>1359079>а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкийСлишком громкое заявление.
>>1359079> а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкий.Ору
>>1359925> Кто-нибудь может объяснить что означает этот дрист?Дрист у тебя в голове, походу. Что ты забыл в этом треде, если простую типизацию читать не можешь? "Сохацький, це тi?" писать сюда пришёл? Иди лучше уроки пиши.
>>1360128Все, я разобрался. Просто беседа в духе> как доказывается ..?> доказательствомНу ОК тут не поспоришь.
> Однажды создатели Coq с удивлением обнаружили, что если в него добавить закон исключенного третьего, то аксиома выбора опровергается. После доработки напильником она больше не опровергается. А мораль этой истории в том, что попытки скрестить слона с китом (ZFC с лямбдами) могут привести к неожиданным результатам. Есть у кого нибудь подробности этой истории?
Покажите, что предикат y = x+1 невыразим в интерпретации (Z, =, f), где f — одноместная функция x -> (x + 2). Не получается автоморфизм построить, автоморфизмы вида x -> kx не подходят, так как f неустойчива относительно них, так же всякие x -> xk и тд. А автоморфизмы вида x -> x +k ничего не дают, так как предикат y = x + 1 устойчив относительно них. И чё делать?
>>1361276Но он активно пилится. И Брэди говорил, что в идрисе не все так однозначно и исправимо. А тут вроде как работа над ошибками.
>>1349231Это каким мегачванливым чмом надо быть, чтобы:1) Обосрать единственный православный редактор2) Посчитать свои поверхностные заметки достойными рецензии (или восхищения?)3) Предполагать, что анонимус не знает, про что говорит, и поэтому несёт чушь
>>1349895>это больше для профессиональных математиков тема, а не разработчиков ПОДа только вот труъ-математикам поебать, а программистам интересно, потому что они пишут свои привычные термы, но вроде бы при этом и математику делают (на самом деле нет). >можно для улучшения качества тестирования использовать эти штукиЭто ну очень оптимистичный взгляд на положение дел. Можно прикрутить рефайнменты с моделчекером или экстрактить из завтипового языка незавтиповой, но корректный код. Что хуже - не знаю, но и то, и другое пока тяжело и долго.
>>1361568>3) Предполагать, что анонимус не знает, про что говорит, и поэтому несёт чушь Естественно. Это так в 100% случаев. И чем более чванливый и безапелляционный тон у высказывания, тем меньше говорящий знает о предмете. Это азы анонимного общения, ти вапще с кокой плонети?
>>1361596Ну на самом деле нет. Бывает, что анонимус может спиздануть, но он это не стесняется признать, если оно так. Картину портят полтора безголовых уёбка, которые находятся в каждом треде и там гадят дико ополоумевши (от них постов больше всего, поэтому кажется, что других нет). А ещё от эффекта разбитых окон вменяемый анон лишний раз склонен промолчать, а то и тоже насрать просто так.
>>1361649> Idris - это говно, которое уже никак не исправить. Просто даже не прикасайся к нему.А что так? Мне он наоборот понравился. Начиная с установки, просто распаковываешь архив и все работает, без всякой дрочьбы вприсядку.
>>1361797Заебал ныть, тебе сложность установки - главный критерий успеха? А пруфы не пробовал писать?
>>1361834Ну, чувак говорит, что иде хуйня, а языки должны стремиться быть такими, чтобы ими можно было легко и просто пользоваться без иде, одним обыкновенным редактором (вместо кодогенерации - более лучшие абстракции, например). В принципе это правильно.А описание имакса тупо устарело - не знаю, может когда-то так и было, но нынче для тех, кто не хочет ничего настраивать, есть спейсмакс.
>>1361846Видел у одного чела который пытался прикрутить агду к вим похожие рассуждения, что кейс-сплиты и подобное не нужны на самом деле при должном уровне просветления. С одной стороны очень похоже на рационализацию, а с другой - довольно любопытная мысль. Может действительно когда есть инструмент начинаешь акцентироваться не на том что действительно важно, а на всякой вторичной поебени.
>>1362154Для меня это очевидно. Вон вкатывальщик написал простыни в начале треда: там только и разговоров про то, как иде работает или не работает. До собственно работы с системами он так и не дошел. Он не понял ни чем они отличаются, ни зачем это все нужно. И все туториалы и проч. тоже на этой чепухе зациклены.
>>1362156>До собственно работы с системами он так и не дошел. Он не понял ни чем они отличаются, ни зачем это все нужно.У тебя какие то болезненные маняпроекции, впрочем, далеко не первый раз вижу тут такое. С каких хуев ты вообще это взял совершенно не понятно. Но да представь себе - перед тем как начать работать с системой ее нужно предварительно установить и настроить, както само-собой чистой силой воли это не делается, приходится поебаться.
>>1362232Ну если бы ты покодировал пруфы и понял, в чём разница, ты бы про это и писал. А поскольку ни до чего интересного не дошёл, то остаётся только изливать анальную боль от того, что не умеешь пользоваться компьютером.
>>1362260>Ну если бы ты покодировал пруфы и понял, в чём разница, ты бы про это и писал.Фантазеры-фантазерчики. Ты сам то чьих будешь - их тех кто расписал весь тред фундаментальными отличиями пруверов (в своем манямирке) или из тех кто даже на пол-шишечки вкатиться не может но воооот задал бы тут всем жару толька ленива чет.
>попробовал я недавно работать в вашем линуксе. Скачал какой-то .iso файл убунты, че с ним делать дальше непонятно. Поискал в гугле, там по-английски чет написано, ниче не понял. Говно этот ваш линукс, удалил.
>>1359079>может вообще один сохацкийВсе, что может сохацкий - это написать элементарный терм из книжки по математике. Ну и еще выложить в инстаграм фоточку с книжкой по алг топологии, иногда открытой на рандомной странице. При это нихрена не понимая материала, естессно.
>>1363305Сохацкий, пидор, вот я крестьянин. Объясни мне, пожалуйста, почему группа точек эллиптической кривой изоморфна комплексному тору.
>>1363360>Ну покажи свой прувер тогдаОчередной аргумент в стиле "сперва добейся".Несмотря на очевидную фриковость всей этой HoTT-компании, у большинства известных участников есть приличное образование, зачастую математическое, и публикации во вменяемых журналах, в том числе по математике и логике. У того же Исаева есть публикации и препринты на архиве.Что там с публикациями у Сохацкого? Тру-математики вообще не знают о существовании такого человека. Все, что он может, это только фоткаться с книжечками, писать простые определения и тригериться на Каледина в твиторе.
>>1363426>Что там с публикациями у Сохацкого?Видел одну (правда в паре ещё с одним человеком); но уже не найду, к сожалению.
>>1363512https://link.springer.com/chapter/10.1007%2F978-3-319-97885-7_30>Recent Developments in Data Science and Intelligent Analysis of Information >Cubical Type Theoryлiл
>>1363426> Несмотря на очевидную фриковость всей этой HoTT-компании, Тыскозал? Ты ж даже не понимаешь что это и зачем, а своё школьное мнение не только имеешь, что ещё полбеды, но и выдаешь за истину, что уже полное школьничество. Сохацкий вас лямбдами обидел, или с чего весь этот хейт?
>>1363610Ну и как можно сравнивать фриковатого Максимку, который может только копипастить чужие пруфы себе в либу, и хорошего, успешного математика.
>>1363642> А Сохацкий?А Сохацкий предложил придумать вопросы, которые он задаст Мортбергу. Только вы даже не знаете кто это, а единственный вопрос, который смогли бы придумать - "Сохацький, це ти?".
>>1363691> Хуи сосёшь? Бочку делаешь?Вот это и есть ваш уровень, дегенераты. И ещё на Сохацкого гоните.
>>1363933 Судя по линкедину, максимка просидел больше 10 лет в кровавом энтерпрайзе, но так и не научился говорить без элементарных ошибок. "I am just interesting", "was came" и тому подобное, и все это украшено постоянным ебанутым смешком.
>>1364001Ну он в принципе и по-русски так же как минимум пишет. Индус же, щито поделать. Главное, что код хорошо пишет.
>>1363933Ебать у них там сборище убогих додиков, у меня годовую норму кринжа переполнило с десяти минут.СУПЕР-ПУПЕР-КОНПУКТЕР-САЕНТИСТ СПЕЦИАЛИСТ ПО ФОРМАЛЬНЫМ МЕТОДАМ@СНЯЛ УЖЕ ХУЛИОН ВИДОСОВ СО СВОИМ ПИЗДЕЖОМ@НИКАК НЕ МОЖЕТ НАСТРОИТЬ ЕБАНЫЙ ЗВУК
Кринжи малолетние, идите нахуй отсюда. Гореть с Сохацкого можно где-нибудь ещё. Вопрос такой: при компиляции в хаскеле сложная типизация компилируется в итоговую программу, или выкидывается? Если код написан с использованием либ типа cubicaltt Мортберга, скомпилируются все функции в полном объёме или нет? Например, в коке при экстракции кода в окамл или хаскел, многое просто выкидывается. Тут не экстракция, но мало ли. Никто не в курсе?
>>1365279>>1365281А разве тогда скомпилированный екзешник будет равен исходному коду? Функции разве одни и теже будут с типами и без?
>>1365448Ну понятно, что по-хорошему надо доказывать эквивалентность исходного кода конечному. Но это задача не первостепенной важности, потому что как раз тут особых проблем не наблюдается.
>>1365451> Ну понятно, что по-хорошему надо доказывать эквивалентность исходного кода конечному. Для этого всякие сертифицированные компиляторы типа CompCert? Но там же тоже типы. Если промежуточные языки типизированы в том же коке для доказательства корректности, а в итоговом бинарнике никаких типов нет, о какой сертифицированной компиляции вообще можно говорить?
>>1365502Транслятор программ из исходного языка в конечный - это функция, к которой можно написать спецификацию и доказательство. Соответственно, можно верифицировать. Конечно, чтобы потом пользоваться этим транслятором, его надо как-то преобразовать в машинный код, а для этого надо опять стирать типы. Ну, ничего не поделаешь, в какой-то момент придётся написать простейший стиратор типов и уверовать в то, что он ничего не портит.
>>1365510Всегда все сводится к тому, что во что-то надо уверовать. И в самой математике так. Это норма, мир у нас такой уж.В верификации все достоинство в том, что нужно уверовать в какой-то конечный кусок кода, который сертифицирует все остальное. Без верификации тебе нужно уверовать в неограниченное количество кода. Причем наперед известно, что баги там наверняка есть - приходится даже не уверовать, а просто уповать на то, что баги не слишком разрушительны. Что самолет не упадет из-за них через пять минут после взлета.
>>1365521> Всегда все сводится к тому, что во что-то надо уверовать. И в самой математике так. Это норма, мир у нас такой уж.Ну нахуй, это не так работает. Я вижу, что суть в типизации промежуточных языков вплоть до машинных инструкций. И далее, если есть доказательства корректности кода в машинных кодах, то и соотв машинные коды без всяких типов будут корректным кодом. А вербовать и без математики можно, для этого пруверы не нужны.
>>1365546Ну ващето, так и работает. Нельзя доказать вообще всё. >Я вижу, что суть в типизации промежуточных языков вплоть до машинных инструкцийНу ващето нет. Типы нужны только в пруверах как средство верификации. В остальных они только для удобства. Можно же (теоретически) сразу верифицированным транслятором переводить верифицированные в том же прувере термы в машинные коды, хотя это непрактично.Можно и сразу программы писать в машинных кодах и их верифицировать.
>>1365572Да, а ещё доказать, что они правильно исполняются процессором, а результат исполнения правильно читается и интерпретируется. Ух сколько всего доказать надо!
> https://tonpa.guru/stream/2019/2019-03-16%20Geometry%20in%20Modal%20HoTT.htm> Я зробив презентацію нашої бібліотеки Groupoid Infinity — усі були у захваті.я представляю себе
>>1371286Да при чем тут математика, ноль информации в твоих каментах.Такое ощущение что ты перед кем-то выйобуешься.Передо мной не нужно, для меня ты никто.
>>1350283>>1351867>>1371583>Сохацкий, це ті? Это такой способ бампать, или вы там все реально ебанутые?
>>1371644> вы там все реально ебанутыеСохацкий, молчи уже. Это вообще не про тебя тред, что ты тут вечно возникаешь?
Вы тута умные, телевизор смотрите поди. Поясните, почему типизация записывается через стрелочку, какой у этих стрелочек смысл? Например, у функции "+" тип Nat -> Nat -> Nat. Понятно, что функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное число (как пример, ясно что складывать можно не только натуральные числа). Это все ясно. А стрелочки нахуя, почему не запятые например?
>>1371734>функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное числоНет. Эта функция каррирована, она принимает натуральное число и возвращает функцию Nat -> Nat:Nat -> (Nat -> Nat) - скобки можно не писать из-за ассоциативности стрелки А функция Nat -> Nat, которую вернет первая функция, уже принимает второе число и возвращает ответ. То есть в выраженииplus 3 5 на самом деле делается (plus 3) 5Где plus 3 вернет тебе лямбду \x -> x + 3. Дальше к этой лямбде будет применена 5 и получен ответ.А то, что ты говоришь, записывается как (Nat, Nat) -> Nat. То есть принимаем пару чисел, возвращаем число. Записываться это будет plus (3, 5). Но так как каррированные функции умеют больше, везде пишут именно их.
>>1371737> Нет. Эта функция каррирована, она принимает натуральное число и возвращает функцию Nat -> Nat:Ок. Ну а тут в чем смысл стрелочки? В логике это импликация, в множествах - отношение подмножества. Или тут смысл не в этом? Тогда в чем?
>>1371741>В логике это импликацияТут тоже что-то вроде импликации, соответствие Карри-Говарда же.>в множествах - отношение подмножестваНе пизди, там не стрелочка.В теоретико-множественной математике вообще функции тоже через стрелочку пишутся. f : A -> B
>>1371746> Не пизди, там не стрелочка.Не стрелочка, но я не об этом, а о том что в множествах отношение подмножества то же самое, что импликация в логике. Т.е Nat -> Nat это импликация, а первый Nat в этой схеме подмножество второго? Хуйня какая-то, не?
>>1371749>Т.е Nat -> Nat это импликацияНе импликация, но что-то вроде. Соответствие Карри-Говарда, google it>а первый Nat в этой схеме подмножество второго?Ну функция задаёт подмножество, да. "Область прибытия" называется
>>1371750> Не импликация, но что-то вроде. Соответствие Карри-Говарда, google itНу пропозишн ас тайпс / сетс. Импликация как подмножество и есть. Я так вижу: в выражении \x -> x + x, "x" очевидное подмножество "x+x" же. Или что?
>>1371762>Ну пропозишн ас тайпс / сетс. Импликация как подмножество и есть. Если утверждения - типы, то импликация - функция.>в выражении \x -> x + x, "x" очевидное подмножество "x+x"Я не понял нихуя, ты занимаешься хуйнёй, что тебе нужно вообще?
>>1349194>В целом вышел весьма поучительный экспириенс, но и довольно болезненный.Я тебе больше скажу — у меня сложилось мнение, что не всегда и автор этих действий сможет их с лёгкостью повторить. Отсюда скепксис по отношению к применимостью в индустрии.
>>1356355Ну если только считать за деятельность копипасты из учебников, лендинги и срачи в твиттерах...
>>1371734>Понятно, что функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное числоНет, функция (+) берет натуральное число и возвращает функцию, которая берет еще одно натуральное число и возвращает натуральное число:(+) :: Nat -> (Nat -> Nat)У стрелочки правая ассоциативность, поэтому скобки писать необязательно.ай блядь, тебе уже ответили, ну похуй, не стирать же>>1371741>Ну а тут в чем смысл стрелочки?Ну функция A -> B берет аргумент типа A и возвращает результат типа B. autism-intensifies Ну A преобразуется в B, стрелочка как бы намекает на это. Что не так-то?>>1371749>Nat -> Nat это импликация, а первый Nat в этой схеме подмножество второго? Хуйня какая-то, не? Ну множество как бы является подмножеством себя, что не так-то? trollface>>1371756>А если функция Nat -> Float ? Ну так ведь Nat подмножество Float, что не так-то? trollface>>1371762>Ну пропозишн ас тайпс / сетс.Ну, функциональный тип (A -> B) соответствует логической импликации (A => B) и теоретико-множественному множеству отображений из A в B. То есть твой тип A -> B утверждает, что из A в B существует отображение, а твоя функция этого типа (любая из них) доказывает это утверждение, приводя пример такого отображения.Ну или вот пример, функция map :: (a -> b) -> [ a ] -> [ b ]. Берет функцию и список и применяет функцию ко всем элементам этого списка, так? Расставим скобки и прочитаем как высказывание о множествах: (a -> b) -> ([ a ] -> [ b ]). То есть: если существует отображение из a в b, то есть и отображение из [ a ] в [ b ]. Логично?>Импликация как подмножествоТы говоришь про то, что подмножество задается так: A ≤ B <=> \forall x : (x \in A -> x \in B), так? Ну так здесь-то у тебя один и тот же x в левой и правой частях импликации, а (Nat -> Float) - это грубо говоря \forall x \exists y : (x \in Nat -> y \in Float), то есть мы в соответствие каждому Nat ставим какой-то Float. И в отличие от примера с map у нас тут конкретные типы (начинаются с заглавной буквы), а не типовые переменные (строчные буквы). Если ты хочешь делать осмысленные утверждения о типах вообще, то тебе и писать надо такие функции, которые говорят о любых типах вообще, а не о Nat и Float. Возвращаясь к твоим подмножествам, \forall x : (x \in A -> x \in B) - у тебя же получается, берет икс одного типа и возвращает тот же самый икс, но уже другого типа. Ну вот например в какой-нибудь джаве ты так можешь сделать, взяв икс и кастанув его к родительскому классу. Ну и нетрудно догадаться, что множество объектов класса-наследника есть подмножество объектов класса-родителя, так ведь?
>>1371837По-моему ты просто завидуешь тому, что человек реально добился успеха в жизни, а ты сидишь на дваче и пишешь "це сохацкий?".
Тоже хочу заниматься математикой в IT, но не унылыми пруверами, а алгебраической геометрий в криптографии: разрабатывать криптосхемы на эллиптических кривых и АГ-коды на эллиптических и эрмитовых кривых. Что надо делать, чтобы это стало реальностью? Где искать работу?
>>1371961>Ну так ведь Nat подмножество Float, что не так-то? trollface>trollface>А если Float -> Nat ? >trollface
>>1371945Не, я только присоединился, но может поддержку движ. Сохацкому не завидую. Немного завидую анону с goviaji. Вот он, как раз чего то добился.
>>1371958Это еще аутичнее пруверов. Работа только в универах. Разработать криптосхему может любой дурак, я вон сам несколько разработал. Толку-то? Нужно понимать зачем, и как гарантировать нужные свойства. А когда начинаешь это нормально понимать, то одновременно понимаешь, что все уже разработано, и тебе уже нечего делать со всеми этими знаниями.
>>1371937Нет. Функция Nat -> Float выделяет в Float некоторое подмножество, изоморфное некоторому подмножеству Nat.
>>1372051Как только зайдешь в хату, ты должен произнести magic cookie и назови свой pid(). Тебе могут бросить под ноги пустое сообщение. Никогда не обрабатывай его handle_call, только handle_info, в крайнем случае handle_cast. Тебя могут спросить кто ты: supervisor, или worker. Никогда не ври, отвечай честно, всё равно все со временем узнают и могут даже exit(Pid, kill), если наврал. Обязательно узнай кто в хате lager.>>1372207Спасибо, теперь понятно.>>1372191>что все уже разработано, и тебе уже нечего делать со всеми этими знаниями.Да и это совершенно нинужно. Любую зашифрованную информацию можно добыть терморектальным криптоанализом.
>>1372207>>1371942>>1371752>>1371746>>1371737>>1371734Начнем с того, что в пруверах используется конструктивная логика Гейтинга, точнее интерпретация логических констант по Брауэру-Гейтингу-Колмогорову (BHK), в которой функция - это примитивный объект (лямбды либо выражения по Мартин-Лёфу), а не декартово произведение множеств определения и значений, как в классической логике и множествах. Изоиорфизм Карри-Говарда для конструктивной логики это то же самое, что изоморфизм без названия между логическими и теоретико-множественными операциями в классической логике и множествах (импликация в классической логике то же самое что подмножество в теории множеств итд). Т.о. возвращаясь к импликации и стрелочкам, в пруверах и прочих хачкелях речь именно о функции в смысле лямбд, поэтому элемент множества A -> B это функция \x.b(x), где x:A и b(x):B. Возвращаясь к функции Nat -> Float, это метод сопоставить натуральному числу или выражению, вычисляющемуся натуральному числу соотв. вещественное число или выражение, вычисляющееся в натуральное число.
>>1372244>назови свой pidСлыш, какой пид нахуй, ты чо бля, ты кого опущенным назвал?А вообще - сохранил, лол.
>>1372321Блеванул с хуеты. Математика это геометрия. Изучение геометрических конструкций средствами алгебры и топологии.
>>1372346Ты опять выходишь на связь, мудило? >Математика это геометрия. Математика это математика. Геометрия это геометрия. Теперь съеби.
>>1348837 (OP)Здравствуйте, я хочу устроиться охранником на овощебазу, посоветуйте пожалуйста какие книжки прочитать?
Продолжаю свои охуительные истории.Решил попробовать по совету анона атом. Ну и думаю нужно отписаться о первых впечатлениях.Установился он сразу с агда-режимом, что это за магия такая не знаю.Какой гений дизайна додумался до серго текста на сером фоне, я ебал.Немного растерялся от подчеркиваний красным в случайных местах но сообразил таки что это ебаный спелчекер. Пришлось гуглить как отключить его. Как же меня вся эта хуйня заебала.Нет подсветки. Ну еб твою мать. Грешен, не так давно отписывался в соседнем треде что она нахуй не нужна и вот она инстант карма. А в агде она бы совсем не помешала. Говорят что нужно ставить отдельный пакет с какого то хуя. Думаю что в таком случае подсветка будет на регулярочках и следовательно точно нахуй не нужна (но возможно ошибаюсь).Но самое охуительное оказалось что атом дрищет под себя от бэкслешей в дырках, пик релейтед. ВОТ ЭТО ПРИКОЛ. Можно конечно там и лямбду написать, но с такого поворота я знатно прихуел. Сколько таких охуительных приколов может внезапно всплыть, так что я подумал да ну его нахуй пока, уж лучше в говноимаксе как-нибудь пока.
Может кто-нибудь объяснить мне что это вообще такое? Не понимаю что это вообще за синтаксическая категория, как там может быть равно и что это значит.
>>1372491алсоВзялся я это доказывать, но рерайты что то не рерайтят нихуя. Только чуть снова сраку не надорвал. (Хотя в принципе я не утверждаю что это невозможно, может быть если кто захочет показать мастер класс буду только благодарен) Заглянул в следующую лекцию и действительно я полез впереди батьки в пекло похоже, потому что МакБрайд доказывает это уже другими техниками. Ух бля думаю почему же это (и это типа сарказм).
>>1372492 еще по мелочи^U ^U ^C ^. - как же я блядь ору с этой хуйни.Хипстеры куда то проебали шорткаты из меню. С другой стороны в имаксе в меню проебали половину команд. Так что в этом плане имеем аксиому Эскобара.>>1371734Интересный вопрос на счет стрелочек в типах. Иногда аргументы отделяются этими стрелочками, а иногда в агде и коке их хуярят просто друг за другом. Вроде должно быть какое то достаточно простое правило когда как, но я его не улавливаю.
Не понимаю такой момент - в категории MAYBE-CAT единичные стрелочки id~> = yes имеют тип T -> Maybe T. Таким образом получается единичная стрелка здесь между различными объектами. Как же так?
>>1372494> Интересный вопрос на счет стрелочек в типах. Иногда аргументы отделяются этими стрелочками, а иногда в агде и коке их хуярят просто друг за другом. Вроде должно быть какое то достаточно простое правило когда как, но я его не улавливаю.Бля, ты разницу между простой стрелкой и П-типом знаешь?
Может некоторые скажут что это тривиально, но для меня было довольно неожиданно что в данном примере параметры C D E как бы прибиндины глобально в скопе модуля и например функтор F имеет тип C => D хотя явно это нигде не указывается.
>>1372502П.А несколько аргументов - это просто вложенные П типы.Π (x₁ : A) (Π (x₂ : A) (… (Π (xₙ : A))…)) : …
>>1372500Подумалось, может быть дело в том что в данном контексте (F >=> G) является ко-паттерном, так ли это?
>>1372872> Получается любой многочлен можно записать в виде функции?Все что угодно можно записать в виде функции. MLTT итп теории типов это же основания математики.
Как в жнумаксе закомментировать/раскомментировать блок агда кода?inb4: никак / установить десяток плагинов и неделю ебстись с их настройкой-настроечкой.
>>1373151>>1373153В саблайме я просто нажимаю ctrl+/ и он автоматически мне комментирует/разкомментирует все что мне нужно. Я так понимаю нихуя такого нет?
>>1373161Попробовал ввести uncomment-region - не работает. Может быть нужно загрузить агду. Загрузил. РАБОТАЕТ. Ну заебок. Несколько минут спустя - повторяю те же самые действия - нихуя не работает. Что это за магия такая?
>>1373161В емаксе есть всё. Только, возможно, тебе самому надо это написать. Ну уж забиндить сочетания клавиш ты сможешь, я в тебя верю
Вот странно. Есть много крутых программистов типа вирусописателей Indy, Pr0mix, Izg0y и других, но на дваче подсасывают и унижают только Сохацкого. Почему все внимание к себе привлекает только разная хуйсосня?
>>1373174>В емаксе есть всё. Только, возможно, тебе самому надо это написать. Ну уж забиндить сочетания клавиш ты сможешь, я в тебя верюПонимаешь, братишка, я пытаюсь разобраться в достижениях компуктер саенса на передней грани человеческих достижений и голова и так уже кипит нахуй. Поэтому у меня нет ни сил ни малейшего желания разбираться с ебаным говноредактором в котором абсолютно все по умолчанию через жопу и нихуя не работает нормально. Нужно всего лишь прочитать томик в несколько сотен страниц документации и проникнуться ебанутой философией в которой нихуя нет но можнозделоть.Но делать то нехуя придется разбираться похоже.>>1373175Они разбираются с -- комментариями, а я пробовал {- -} раскомментировать. Но это не важно, не знаю что я должен был вынести из этого обсуждения по-твоему. Я понял только то что у них нихуя не работает, но этим меня уже не особо удивишь.
>>1373207>я пытаюсь разобраться в достижениях компуктер саенса на передней грани человеческих достижений Не понял, а агда тебе зачем тогда?Жми Alt+; и не будь тупым, заколебал
>>1373209>Жми Alt+; Жму - добавляются -- в конце строки - ору с прыщефункциональности>и не будь тупым, заколебалне будь батхертом
>>1373214Ну значит холоп, разработавший agda-mode, не позаботился об удобстве для тебя-барина. Живи теперь с этим.
>>1373215Мне просто неприятно видеть как вроде бы неглупые люди уплетают куски кала и визжат от радости. Но полагаю каждому свое.
>>1373216Да, вот уж какая неприятность. Компьютер саентинст позволяет себе такую дерзость, как вместо занятий компьютер саенсом писать плагины для текстовых редакторов, чтобы какому-то уёбку с двачей было поудобнее черкаться, чтобы он через неделю бросил. Как страшно жить.
>>1372321Отче наш, Мартин-Лёф!Да святится имя твое, да придет интерпретация логических констант по Брауэру-Гейтингу-Колмогорову;Да будет изоморфизм Карри-Говарда на небе и на земле;Хлеб наш конструктивный вычисли нам днесь;И прости нам тезис Черча, как и мы прощаем исключенного третьего должникам нашим;И не введи нас в интуиционизм, и избавь нас от невычислимого.MLTT.
>>1373789>>1373873Правильно, семенсеменыч, сам себя не похвалишь - никто не похвалит. Только не говори, что у такого убогого петуха как ты есть ещё более убогие подсиралы.>>1373688Гениально. Апплодирую стоя хуем тебе по лбу.
>>1374460Конструктивист должен знать:- изоморфизм Карри-Говарда и тезис Чёрча;- содержание диссертации Брауэра в переводе Гейтинга;- пять уровней языка и четыре способа отрицания по Маннури;- интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;- теорию статистического обучения Вапника и модель spikgram Миколова;- отличия машины Тьюринга от машины Поста.Конструктивист обязан:- отрицать закон исключённого третьего;- отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;- переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;- представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;- свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
>>1374538> - отрицать закон исключённого третьего;Гугли теорему Дьяконеску, эту скрепу можно доказать конструктивно.> свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.К cubicaltt ваши гамалогии уже сводят. Не очень активно, но примеры есть даже у Мортберга на гитхабе. Тебе ж говорят, мань, вся математика по своей сути конструктивна, если что-то ещё не доказали в пруверах, значит этим просто некому заниматься.
>>1374759> Ты узнай что такое гамалогии сначала, патом уже своди.Мне твои гамалогии в хуй не стучат. Я говорю, кому это интересно, уже делают.
>>1374760>вся математика уже конструктивна>мне твоя математика в хуй не стучит>не очень активно, но делают
>>1374770>>1374828Ты еблан, реально. Какие тебе гамалогии, ты русского языка не понимаешь, хотя являешься носителем. Может быть хоть отсюда сьебешь? Гореть можно где-нибудь ещё.
>>1374770>>1374828>>1374851Когда люди не понимают тебя, они не думают что они тупые, они думают что ТЫ тупой (с) Конфуций
>>1374934Diaconescu theorem же, все гуглится. Даже видос на ютубе есть. https://www.youtube.com/watch?v=21qPOReu4FI
Напыщенные математики послали сюда. Дублирую вопрос.Хотелось что-нибудь почитать фундаментальное о формальных системах, как-то связать это с программированием, так как я программист. Объясните нубу, с точки зрения математики эти вещи потеряли актуальность с появлением HoTT. Например если хочется математики то нет смысла читать Введение в математику Клини, а нужно читать HoTT? Подозреваю, что этот вопрос всех заебал, но все-таки.
>>1374748>эту скрепу можно доказать конструктивно.Аксиому выбора уже доказал? Только в классическом виде, не конструктивную псевдоаксиому.
>>1378221> Аксиому выбора уже доказал? Только в классическом виде, не конструктивную псевдоаксиому.В MLTT это не аксиома, а доказуемая теорема. Мартин-Леф доказал. И именно в том смысле, как она понимается в ZFC, только классически, в ZFC она недоказуема, поэтому классически в неё предлагается как раз таки уверовать.
>>1378212> Объясните нубу, с точки зрения математики эти вещи потеряли актуальность с появлением HoTTНет, не потеряли. Более того, не зная азов, ты и HoTT не поймешь. > Хотелось что-нибудь почитать фундаментальное о формальных системах, как-то связать это с программированием"Programming in Martin-Lof type theory", например, но с нуля такое не зайдет. Хотя бы о матлогике нужно иметь представление.
>>1378231О мат логике представление есть. В вузике даже что-то типа теории формальных языков было. Но я уже нихуя не помню
>>1378212Переформулирую вопрос. Как вкатиться, чтобы понимать принципы того, чем я занимаюсь вообще связь программирования с математикой, какие-то определения, что такое вычислимость вообще и т.д. Software Foundations? Ну и конечно хотелось бы и основания математики понимать, а это как я понимаю HoTT теперь, или неправильно понимаю?
>>1378235> связь программирования с математикойИзоморфизм Карри-Говарда.> какие-то определения, что такое вычислимость вообще и т.д. В вышеупомянутой книжке >>1378231
>>1378235> Software Foundations? Вполне. Для агды ещё PLFA. > Ну и конечно хотелось бы и основания математики понимать, а это как я понимаю HoTT теперь, или неправильно понимаю?HoTT очень сырая. Та же аксиома унивалентности Воеводского в ней недоказуема, доказать её можно в cubicaltt, ещё более сырой. Это не те темы, с которых нужно вкатываться.
>>1378241>Та же аксиома унивалентности Воеводского в ней недоказуемаНу и? HoTT Book - всё равно - всё ещё самый крупный источник по теме. И написана книжка очень хорошо. А сразу с Cubical Type Theory никто начинать не будет.>доказать её можно в cubicaltt, ещё более сырой.Не только, в шапку посмотри.
>>1378237>Изоморфизм Карри-ГовардаВ какой категории этот "изоморфизм"? Три года уже пытаемся выяснить это с пацанами из /math, ты всё никак ответить не можешь.
Бампецкий вопросам >>1372491>>1372496Почему стоит только спросить хоть что то немножко посложнее "посоны хачу вкотиться!111" всех икспертов как ветром сдувает.
>>1378549Нахуй эта игра в кошки-мышки, пиши прямо что и как, не будь гнилым пидорасом, можешь это для своих студентиков оставить, которые тебя на хуй послать не могут.
>>1378380> В какой категории этот "изоморфизм"? Три года уже пытаемся выяснить это с пацанами из /math, ты всё никак ответить не можешь.С воображаемыми? Ты один такой ебнутый, мань.>>1378553> Это типа доёбка до слова "изоморфизм", вместо которого должно быть "соответствие"?Будто не одно и то же.>>1378738> Конструктух такой конструктух.По делу возражай, пукнутый, или мимо иди.
>>1379483> Как доказать modus ponens?Элиминатор импликации, ты хотел сказать. Построением пруф-обьекта, удовлетворяющего этому правилу вывода, очевидно же. "Модус пони поненс" это что-то из Аристотеля, доказательство - онскозал.
>>1379483модус поненс это правило вывода взятое за основу. Как аксиома. Это не работает так что "Вот просто это правильно и примите это". Это работает так "Если мы возьмем модус поненс и несколько аксиом, то сможем вывести такие логические заключения". Ты можешь взять любое другое правило вывода и другие аксиомы и получишь свою аксиоматическую систему. Вопрос в том будет ли она выводить те же логические выводы, что и ты. Она может будет выводить что-то типа "Если конь животное и нефть топливо, то Топливо конь"
>>1379671Я давно не писал на агде, поэтому могу ответить на вопросы только по коку.ЧИТАЙ ЁБАНЫЙ МАНУАЛ КУСОК ГОВНА ТАМ ВСЁ НАПИСАНО
>>1379685Очень даже по делу. Ты не читаешь ёбаный мануал и просишь, чтобы кто-то другой почитал и объяснил тебе. Ты жалок.
Справедливости ради, в мануале есть не все. Нотация в агде типа {B : A -> Set} для характеристической функции B a [a : A], например. У Мартин-Лефа тоже не написано, что в таком случае B : A, только в одном месте вскользь упомянуто, что характеристическую функцию можно интерпретировать как подмножество. Конечно, можно и догадаться, что в этом случае В это подмножество А, т.к все элементы В принадлежат А. Но по хорошему, в правильной нотации не должно быть такого, что нужно что-то додумывать.
>>1379754Как это `B : A -> Set` и `B : A` одновременно? Кроме того, характеристическая функция - это же объект изоморфный подмножеству, а не оно само.
>>1379754>>1379766О каких "множествах" вы вообще говорите, совсем ебнулись? В программульках нет никаких множеств, это только в математике.
Подумываю вкатиться в верификатора. Поясните что это за ебала такая и какие подводные?что за> алгоритмы ЦОСпомню в вузике изучали z-преобразование, какая то полная ебала бесполезная. Так то и кодеки ведь тоже "ЦОС", какое-то широкое понятие.
>>1379766> Как это `B : A -> Set` и `B : A` одновременно? А вот так. https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers> Кроме того, характеристическая функция - Пропозициональная же. Совсем заговорился.>>1379774> О каких "множествах" вы вообще говорите, совсем ебнулись? В программульках нет никаких множеств, это только в математике.Тыскозал? Про MLTT не слышал, что ты тогда в этом треде потерял?
>>1379869Что-то я всё равно ничего не догнал.1. B : A -> SetB - это семейство типов, индексированное типов A. Оно задаёт подмножество в типе А (те индексы, для которых соответствующий тип населён). Если бы в агде было элементарное отношение подтипа :>, и было бы верно B :> A, это, конечно, здорово, но вроде нет такого, потому что это не умещается в теорию (хз почему).2. B : AB является элементом в типе А. Вот как это вообще связано с 1? При чём тут информация, доступная по ссылке, тоже не понял. Там из чего-то следует, что стрелочный тип может каким-то образом стать нестрелочным? Или что у одних и тех же переменных может быть два типа, один стрелочный, другой нет?
>>1379869>MLTTТеория множеств Мартина-Лефа, а не что то по буковкам не сходится никак. Подучил бы ты уже мат-часть, конструшок, сколько можно поносом под себя дристать.
>>1379897> Теория множеств Мартина-Лефа, а не что то по буковкам не сходится никак. Подучил бы ты уже мат-часть, конструшок, сколько можно поносом под себя дристать.Тебе за шиворот поносом надристал. И андеркатом твоим из барбишопа жопу вытер. Изоморфизм Карри-Говарда, маня, пропозишены как типы / множества. Я уже объяснял, когда типы могут рассматриваться как множества, а когда не могут. Это прямо следует из определения множества в MLTT. И если тип с вычислительной точки зрения задан как множество, то в данном случае он и будет множеством. Если ты этого понять не в состоянии, проблема в тебе, а не во мне и не в MLTT.
>>1379881> B является элементом в типе А. Вот как это вообще связано с 1?И подмножеством А. Т.к все элементы В это элементы А.
>>1380166> "Элемент" и "подмножество" - разные вещиВ данном примере - нет.> . Да и элементы B - это функции, а не элементы A.Элементы пропозициональной функции В это таки элементы А.
>>1380121>Я уже объяснялЛол, петух все на своей волне.ОК, пополнил словарик петушиного:математика - вычисления, они же - рефлексыкризис математики - теоремы Геделяаксиома - это не аксиомаотличие актуальной бесконечности от потенциальной - я все это сто раз объяснялформализация - проблема остановамножество - тип
Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему. Дискасс.
>>1380243Я не виноват, что ты настолько тупой, что даже просто механически пересказать мои слова не в состоянии, не говоря о том, чтобы понять. Почитать источники, на которые я ссылаюсь ты не можешь, потому что там какие-то буквы нерусские,это я понял. Я вообще не представляю, что тебе от меня нужно и с какой целью ты за мной бегаешь по всему мейлру года 3 уже как. В каком месте я тебе настолько больно сделал, чтобы вызвать такую злокачественную батруху?
>>1380256Лол, конструктух в своем манямирке правда думает что какой-то негодяй бегает за ним 3 года и не понимает что над ним орет половина мейлру.
>>1380268Нет, мань, таких дебилов тут 1,5 клоуна максимум. Причём, возражений по существу от вас так и не поступало. А препирания уровня детского сада с каким-то унтерменшем (или с двумя, что то же самое) мне неинтересны.
>>1380257> Опиши кванторыА что его описывать? В пропозициональной логике квантор и является пропозициональным знаком. Такой символ нельзя сказать, его можно только показать.
>>1380607>Added a new sort Prop of definitionally proof-irrelevant propositions.Такая же хуитка как в петухе? Которая хуй пойми зачем нужна и вообще "was a mistake" по мнению некоторых.
>>1380763В петухе немного не очень, потому что там реальная иррелевантность только в разрешимых случаях, если не добавлять аксиому К. А в агде без аксиомы нормально теперь.
>>1380766>аксиому ККакие такие аксиомы, ведь швятой Браузер и пророк его Мартин-Леф так зделали что никакие аксиомы не нужны а все на рефлексах делается? Срочно вызываю конструктивного петуха в тред.
>>1380774Ты что еще не уверовал? Покайся грешник пока не поздно, а то изоморфизм Кари-Говарда тебя накажет!
>>1380773Пишешь флаг --without-k и нет никаких аксиом. Или сразу пишешь на коке, там по умолчанию нет.
>>1380906>А это и не аксиома, просто название такое Сверился со словариком на всякий случай:>аксиома - это не аксиомаи правда, все сходится!А что же тогда интересно?
Объясните мне кто-нибудь максимально популярно - кого и для чего может вообще ебсти что два рефла или вообще доказательства равны между собой или нет? Ну вот реально на практике какие возникают затыки?
>>1381051Меня лично отсутствие равенства бесило когда я делал структурки с пропами. Например, есть две алгебры с одинаковыми носителями и одинаковыми законами. Но равенство их доказать не можешь, потому что пропы, хотя по смыслу равенство имеет место. И приходится везде таскать разрешимость на носителе как гипотезу, а это нахуй надо? Ну или K прописывать.
>>1381058>Например, есть две алгебры с одинаковыми носителями и одинаковыми законами.Почему бы тогда не выбрать один вариант и использовать его? смекалочка
Я беру и пишу тип Nat. А потом пишу тип HuiNat. Потом пытаюсь написать zero=huizero но ничего не получается ((((( Поможите люди добрые придумайте систему типов чтобы все работало как я хочу.
>>1381488Разве там равенство не только между объектами одного типа?В любом случае, это сарказм был жи, в том плане что я не представляю на хуя это вообще нужно.
You might wonder why we do not just write the following for this theorem:∀ {x y z : ℕ} → x < y → y < z → x < zThis looks more elegant, because we do not have the “≡ tt” everywhere we areusing _<_. But this expression will not type check, because as defined in the IAL,_<_ returns a boolean (), and a boolean cannot be used as a type.А такую оказию передовые разработки теории типов способны разрешить? А то кукарекать про изоморфизмы горазды, а вдруг хуякс и надо все по два раза писать один раз для Set (Prop) другой раз для (bool). Еще бы нормальный полиморфизм для явных-неявных аргументов завезли. Или это НОРМА и по-другому никак? Надеюсь что не оскорбил чьи то нежные чувства этим вопросом в очередной раз.
>>1382006Стоишь на асфальте, в лыжи обутый. То ли лыжи не едут, то ли ты ебанутый. Ты нормально перепиши ,тогда будет тайпчек проходить. Очевидно же, что _<_ не совсем то, что тут нужно. Но, это конечно же, изоморфизмы виноваты и лично Мартин-Леф. Пиздец ты клоун.
>>1382006Типы и функции - не одно и то же, очевидно, поэтому надо сначала написать одно, потом другое, потом доказать эквивалентность и пользоваться этой эквивалентностью где хочешь. Set (Prop) и bool сильно разные по смыслу, так что ничего удивительного
>>1382006В приципе-то, можно было придумать штуковину, которая залезает в кишки разрешающей процедуре и восстанавливает из неё тип с подходящей алгеброй пруфтермов. Но это чисто механическая вещь, которая не относится к самой теории, где-то на уровне тактик и солверов.
Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему.
>>1382233> Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему.
>>1382125>Ты нормально перепиши ,тогда будет тайпчек проходить.Ты че совсем ебанутый, умственный инвалид блядь, это ж пример из книги, я должен что ли писать автору - все хуйня, срочно издавайте второе издание.>Но, это конечно же, изоморфизмы виноваты и лично Мартин-ЛефНу когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.>>1382147>Set (Prop) и bool сильно разные по смыслуВот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.>>1382151>Но это чисто механическая вещь, которая не относится к самой теории, где-то на уровне тактик и солверов.В агде обычно ведут речь о том что вычисления и мета-вычисления живут в одной реальности. Как минимум хотелось бы этого в идеале.И вообще я вижу тут стандартный набор из гнева, отрицания, торга. Можно было в таком же ключе сказать > есть тип list of nat а есть тип list of bool и как ты один в другой засунешь, ты что ебанутый? Поли-чего блядь, че несет. Не ну можно написать шаблонизатор который подставляет текст, может быть.
>>1382543> Ну когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.Над этим школьным бредом даже не орать хочется, а посочувствовать губошлепу, который это пишет. Ощущение у него складывается. А у тебя не складывается ощущение, что если против MLTT во всем мире копротивляется ровно один залупок из северной Нигерии, то проблема может быть и не в MLTT вовсе? Или это слишком сложно для тебя, а, ниспровергатель подпивасный?
>>1382543>Вот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.Ну да, просматривается, хотя это, строго говоря, совсем не изоморфизм. Проблема в том, что в каждой конкретной ситуации этот самый изоморфизм надо прописывать руками.>В агде обычно ведут речь о том что вычисления и мета-вычисления живут в одной реальности. Как минимум хотелось бы этого в идеале.Хотелось бы, конечно. Не надо забывать, что пруф ассистанты - это work in progress, и разумно было бы сперва найти хорошие теоретические основания, подходящие для практики, а уж потом все удобства, свистелки и перделки.>> есть тип list of nat а есть тип list of bool и как ты один в другой засунешь, ты что ебанутый? Поли-чего блядь, че несет. Не ну можно написать шаблонизатор который подставляет текст, может быть.Ну всё правильно, либо ты сам пишешь руками вложение одного типа в другой, либо пишешь механическую процедуру, которая за тебя это делает, если это возможно. Вообще непонятно, а хули ты хотел-то?
>>1382543>Ну когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.И вообще-то, конечно, ты тут наёбываешь сам себя, потому что Set (Prop) - это и есть логика, а bool - это всего лишь тип результата для разрешающих процедур. Если вопросы разрешимости тебя не беспокоят, можешь выбросить этот bool нахуй и писать в типах. Если наоборот, только они и беспокоят, можешь выбросить логику. А если всё-таки надо усидеть на двух стульях, как это часто бывает, пиши и то, и другое, и доказывай эквивалентность.
>>1382643"вычисления и логика - одно и то же", конечно, означает только то, что истинностные значения утверждений и результаты вычислений живут в рамках одной теории и выражаются одними и теми же сущностями (типами). Разумеется, нет речи о том, что тип вычисления и тип какого-то связанного с ним утверждения совпадают. Если кто-то где-то сказал тебе иное, то да, тебя наебали.
>>1382543>Вот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.Для построения такого изоморфизма нужен LEM.
>>1382603>>1382543>умственный инвалид>Вообще непонятно, а хули ты хотел-то?Ну, все сходится.>>1382744Хуйню написал.
>>1382783Шлите нахуй дегрода. Ничего ты этому хуепутолу не докажешь. У этой хуеты два мнения - одно его, другое неправильное.
>>1382810Может пойдешь уже подошьешь свой порванный анус, а то заебал уже им тут трясти, может ведь и нагноение начаться.
>>1383530Ясно, отбитый тупица пытается рыпаться, ссу на кретина не способного даже в элементарную логику Аристотеля, но чего то там кукарекающего о высоких материя.
>>1384154Ты только себе на ебало нассал, долбоёб.Или ясно докладывай свою позицию, или уёбывай отсюда.
