Coq:
https://coq.inria.fr/
Lean:
https://leanprover.github.io/
https://github.com/leanprover/lean4 (компилируется в кресты).
Agda:
https://github.com/agda/agda
Idris:
https://www.idris-lang.org/
HoTT:
https://github.com/HoTT/HoTT
https://github.com/HoTT/HoTT-Agda
https://github.com/gebner/hott3
Cubical Type Theory:
https://github.com/mortberg/cubicaltt
https://github.com/mortberg/yacctt
https://github.com/RedPRL/sml-redprl
https://github.com/RedPRL/redtt
https://arend-lang.github.io/
agda --cubical
>Прувер
О чем тред?
Сынок, ты не понял. Это — борда для обсуждения ковариантных функторов, анафорических макросов, пандорических захватов, кластеров метапарадигм, катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов, ненужности математики, наконец. Никого здесь твои слесарские проблемы не волнуют. Ваш жалкий практический земной мирок не нужен. Съеби.
Зачем ты такие треды создаешь в белом интернете, это незаконно вообще то.
И зачем? Тут никто ничего нового и не прочитал ещё. Приходи через пару лет.
В Lean это вот так делается, например: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md
Для кока гуглятся только какие‐то анальные методы: https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html, http://www-sop.inria.fr/members/Yves.Bertot/tsinghua/tsinghua-5.pdf
Вот ещё интересное: https://stackoverflow.com/questions/33302526/well-founded-recursion-in-coq («You will then have to provide a proof that the arguments used in the recursive call are smaller than the top level ones according to the measure».)
Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
natU 0 ≔ ⊤
natU _ = ⊥
th : 0 = 1 → ⊥ -- aka 0 ≠ 1
th prf = coe (ap natU prf) ★
по порядку:
ap natU prf : ⊤ = ⊥ | ap : (f : a → b) → x = y → f x = f y
tr (ap natU prf) : ⊤ → ⊥ | coe : A = B → A → B
tr (ap natU prf) ★ : ⊥ | apply
>Arend background.png
\У \куска \говяхи \синтаксис \лучше
> Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
То, что у тебя нет мозгов, потому что ты зумер, не значит, что их нет ни у кого.
Ой дибил... дерево вывода где? Где аксиомы? Ты просто веруешь.
алсо
>>1516026
>То, что у тебя нет мозгов, потому что ты зумер
у убогих мандавошек проекции просто одна охуительнее другой.
>>1516070
>Проблема унивалентных оснований даже не в том
>можно использовать только при наличии бесконечной памяти
Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время". Хотя думаю нет - они ж были совсем не тупые как местная пидорва.
Нужно и равенство да, но если есть индуктивные типы для чистого исчисления (Cedile), то можно элиминаторы равенства и его бета (J) и эта правила (которое в не HoTT системах запрещено) написать в чистых функциях. Так то дед! Ты не совсем дибил если знаешь про J, но явно отстаешь от индустрии лет на 5.
Ну вот мы и видим как еще один верун дристанул под себя. Естественно никакого дерева вывода можно не ждать, ведь ты не имеешь ни малейшего понятия как работает твоя система, а просто в нее веруешь.
>для чистого исчисления (Cedile)
>дает доказательство в lean
Максимальная маневренность. Хотя до чудика выше что дал доказательство в собственном маня-mltt еще далеко.
Ты просто ни разу NbE не написал и живешь в бумажных деревьях, математик которые не может в дебагере выставить printf будем вопить и плеваться на анонимных досках, потому что в то время пока он будет рисовать никому не нужную макулатуру на бумаге, программисты будут писать за него теоремы о неподвижной точке.
Вопрос: докажите 0 ≠ 1.
Пруверо-пидорва: ссытся под себя и пускает слюни от собственной беспомощности.
Ясно.
У тебя ж два доказательства на руках, на Agda и на Lean. Или у тебя проблема какая-то в коммуникации и ты не можешь прочитать книжку и вместо своего СДВГ ты лезешь в интернет и орешь "это не доказательства!", "Арнольд говорил компьютеры не нужны!". К чему это все? Мы можем тебе написать доказательство 0!=1 на всех MLTT языках не вопрос. Но во-первых ты не принимаешь эти доказательства. Я слабо верю в то, что ты не веришь что существует изоморфизм между генценовскими палочками и трейсом работающей программы на компьютере. Ты либо просто ебанутый либо человек с нарушенными коммуникативными способностями.
>У тебя ж два доказательства на руках, на Agda и на Lean.
На агде можно вроде бы проще написать в одну строчку, за Lean-поебень не скажу. В коке я могу вообще одной командой это сделать - inversion - и готово, охуеть да как ловко? Только я спрашиваю на каких фундаментальных принципах основываются эти доказательства. Проблемы не с моими
>коммуникативными способностями
а только с мыслительными способностями местной пидорвы. Они даже не понимают о чем их спрашивают. "Ну раз система говорит что это так значит это так" - верунчики, что с них взять. Особо продвинутые еще могут про швятой изоморфизм спиздануть не к месту.
>ты не можешь прочитать книжку
>своего СДВГ
>Арнольд говорил компьютеры не нужны!
новые потешные проекции подоспели.
А вот возьму и построю. Ты то что будешь делать, манька, так и будешь продолжать веровать и молиться швятому автоматону?
>>1516710
>То он Арнольд, то воинствующий Кок-петушок уже.
Манька запуталась в собственных маня-проекциях, так мило.
>>1516713
И что они там делают, рассказывают MS-блядям что уже есть система для нормальных людей? Накидай линков что ли.
Это чисто математические тусовки, там даже математиков с ноутами на винде нет. Это спонсируется грантами евросоюза. Ну если ты можешь построить Модельнеые категории для инфинити топоса на слабых расслоениях симплициальных множеств, то уже будешь 6-й в списке тех, кто это сделал.
Даже не 6-й, а 8-й уже.
> Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время".
Для их нотации время давно прошло. Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
>где аксиомы?
Аксиомы Lean?
https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf
>дерево вывода где?
Вон тебе бумажка, сам выписывай. Я ебал такой хуйнёй заниматься.
>Ты просто веруешь.
Верую во что?
В то, что авторы Lean действительно написали то, о чём рассказывает та бумажка? Да, верую, не разбираться же мне в тоннах крестокода.
В то, что существуют контексты и переменные? Да, верую, что тут такого?
В propext? Да, верую, но в чём проблема?
В choice? Если надо, тоже уверую.
До чего ты доебался, петух?
>Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
О, неужели конструктивный петушок показал свой клювик с подпевалами? Давай расскажи мне как конструктивная математика не нуждается в аксиомах потому шта она естественно правильна ведь там математики все делают на рефлексах и не могут ошибаться. А конпункторы у них хоть и рефлексов нет но они там что то вычисляют а раз оно что то там вычисляет значит у утверждения есть ВЫЧИСЛИТЕЛЬНЫЙ СМЫСЛ следовательно оно не может быть не верным. Как то так. Посмеши деда еще. Можешь про неформализуемость алгоритма ведь ТУЮРИНГ ПРОБЛЕМА ОСТАНОВА ГРОБ ЧЕРВЬ ПИДОР в своем манямирке спиздануть, очень потешно.
Что сказать-то хотел, чучело? Горелым пердаком по всему мейлру трясти у тебя время есть, а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету? Ну кукарекай дальше, если тебе это интереснее, чем хотя бы попытаться разобраться в теме, дело твое. Просто свое место у параши не забывай, твои победоносные кукареканья не делают тебя умнее создателей конструктивной математики, не забывай этот простой факт.
> Посмеши деда
Говна на обед поел уже, дед?
>>1516979
Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
>Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
Ты снова проецируешь, конструшила?
>а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету?
Я кстати пытаюсь почитывать швятые писания, удерживая рвотные порывы, но таких "вершин" как конструктух мне никогда не достичь, потому что - паста
> понятно только ебанутым ... подобно тому, например, как христианам понятно как женщина была сделана из ребра мужчины, в то время как ни один нормальный человек такой хуйни никогда не поймёт просто потому что он нормален, а не ебанут
Если длинно, то Coq всегда был фреймворком для разработки тактик с удобным сопряжением со внешним миром. Lean в этом смысле более народный из-за С++ и в то же время более быстрый. В отличии от Coq, у Lean достаточно простое и понятное ядро, гораздо легче писать тактики, не нужно учить ocamlp5 и 4 промежуточных языка для этого. В Lean вкатаны уже достаточно интересные вещи типа перфектоид пространств, а все что вы можете найти на коке это либо старье либо как когда-то писали деды.
Тебе срачелу разворотить например. Вижу что результат весьма неплох.
>>1517079
Хороший самоподдув
>>1517102
>4-я версия Lean уже будет обладать макросистемой и self-hosting, поддерживать FFI в С/C++, можно будет писать свои веб сервера, консольные приложения, и проганять ваши теории на промышленных датасетах прямо в производстве на полях.
>СУПЕРКОМПЬЮТЕРЫ БУДУТ РАЗМЕРОМ С ТЕЛЕФОН, ТЕЛЕФОН С ИНТЕГРАЛЬНУЮ СХЕМУ, ИНТЕГРАЛЬНАЯ СХЕМА С НАНОРОБОТА, А НАНОРОБОТЫ В КАЖДОМ ПРЕДМЕТЕ БУДУТ СИДЕТЬ И ПЕРЕСТРАИВАТЬ МАТЕРИЮ НА СУБАТОМНОМ УРОВНЕ!
Ага и обратная совместимость по пизде пойдет и все
>интересные вещи типа перфектоид пространств
по пизде пойдут
Кто-нибудь знает, x86 ISA верифицирована? Как там с доказанной корректностью процессоров, вообще?
Дефект по типу «второй жизни» определяется тотальными странностями, распространяющимися на все сферы психической деятельности: эксцентричность внешности и речи, парадоксальность и дефицитарность эмоциональной сферы, достигающие степени регрессивной синтонности отношения с окружающими, полностью замещающие профессиональную деятельность аутистические сверхценные увлечения, – и сочетается с психопатоподобными расстройствами иного круга (зависимые, истерические) и псевдоорганическими/астеническими нарушениями.
При этом происходит переосмысление и ревизия системы ценностей, прежде всего относящихся к конвенциональной деятельности: прежние, социально значимые интересы (учеба/работа) отчуждаются и обесцениваются, подменяясь патологическими сверхценными увлечениями
Основным содержанием жизни (сверхценное мировоззрение при изменениях типа фершробен [Аведисова А.С., 1988; Birnbaum K., 1906]), становятся «патологические сверхценные увлечения» [Сергеев И.И., Малиночка С.А., 2008] с идеями реформаторства или собирательства – странные, оторванные от реальности хобби, выступающие в качестве проявлений односторонней аутистической активности и носящие характер необычных, подчас лишенных всякого смысла, не приносящих дохода увлечений
Аутизм - чек, нездоровые отношения с коллегами - чек, двойная жизнь - чек. В жизни это крудошлеп, боящийся сокращения, который 24/7 разгребает таски, а на двачах это успешный технофилософ каратель анальников.
Оба языка считаются "быстрыми", так что все зависит от криворукости писавших. Можно даже допустить что что-то там на lean работает быстрее и какое-нибудь мега-доказательство будет верифицироваться на lean всего два машино-месяца вместо четырех на coq. Вот только мне от этого совсем не легче когда я запускаю lean и оно у меня моментально отжирает гигабайты памяти, грузит проц на все сто и падает.
> Видно, что умы авторов языка пребывают в каком-то астрале, слабо связанным с такими земными вещами, как клавиатуры, глаза, эстетика.
Суть этих языков не в том, чтобы наиндусить как можно больше говнокода. Задача нотации - быть максимально прозрачной и близкой к общепринятой математической, для чего в той же агде поддержка юникода https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html
>Суть этих языков не в том, чтобы наиндусить как можно больше говнокода.
Так и про брейнфак можно сказать.
>Задача нотации - быть максимально прозрачной и близкой к общепринятой математической
И как в этом помогает \where?
Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Что значит «слишком сложен»? Я привел характеристики языков по значимому для меня набору критериев. Я осознаю, что существуют безмозглые пидоры, у которых в список значимых кримериев может входить, к примеру, синтаксис языка. Hу так накласть мне на них. Меня интересуют объективные критерии, а не цацки всякие.
(с) vsl
>Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Просто два чая этому любителю прекрасного.
Вроде бы скрываешь треды, а через некоторое время, когда они почти утонули, кто-то их бампает, и они опять появляются. Почему так?
Что это за азиатский монстр? Как столько всего можно знать в 19 лет? В 16, судя по коммитам он уже спокойно вертел avl деревья, пилил свои компиляторы и свободно владел парой десятков языках, ТК он также отлично знает, а сейчас устроился на позицию пруф чекера в жидбрейнс. Он гений или просто убер-задрот? Или всё вместе?
А какая практическая польза ото всего этого?
Toolbox медленный и работает коряво, например иногда курсор перескакивает куда попало, что меня несколько раздражает — есть ли ему достойные альтернативы?
Ссаный тред подёнщиков, которым никогда не откроются тайны бездонного моря алгебраической геометрии.
Нахуй вы это учите?
> Я правильно понял, что это просто движок, который умеет делать преобразования на языке мат.логики, и может размотать изначальное выражение и проверить, приходит ли оно к тому, что надо доказать?
Как-то так, да. Ибо пикрелейтед.
> насколько эти движки скилловые? В смысле, мат.логика - это далеко не все.
Даже йогурты не все одинаково полезны, про матлогику и говорить нечего. Но касаемо HoTT и CuTT - это как раз правильное направление матлогики, про которую нельзя сказать, что она "далеко не все".
> В процессе доказательства привлекаются самые разнообразные методы, в том числе и прямые математические расчеты(выражения и их численные значения), и различные продвинутые методы, даже иногда графические.
Все это (и не только это) тривиально сводится к типам.
> Та же теорема Ферма, доказанная через эллиптические кривые - никому ведь ранее даже в голову не приходило связать одно с другим.
Эллиптические кривые - всего лишь тип в инфинити групоиде, изоморфных которому там полно. В том числе таких, использовать которые в доказательстве теоремы Ферма никогда не придет в голову вообще никому и никогда, потому что мозгов не хватит.
Как прикрутить это все к c++?
Настоящие математики-профессионалы ссут на вашу теорию типов
(sqrt(2) == 1.4142135623730951) == false
Иначе говно без задач.
https://pastebin.com/eQ5Db3pV
Жопой чую можно лучше
Таки жопа была права.
https://pastebin.com/3rvdUwYU
Тредик живи!
Тут кто-то есть о_О.
https://pastebin.com/npJYLv0g
Очень интересная аутистская ерунда! Какую самую сложную теорему вы формализовали? Или доказали? Я просто еще не до конца понял, что тут происходит.
https://github.com/idris-lang/Idris2
> llvm бэкенд планируется?
Можно в С скомпилировать, а из него clang'ом в LLVM.
>>1697197
> Но это было будущее 20 лет назад. Оно плавно стало прошлым, так и не пройдя стадию настоящего.
Манямир. 20 лет назад про зависимые типы знали полтора математика из coq комьюнити. На идрисе сейчас обкатывается то, что в яп будет нормой лет через 10 минимум.
> idris -> c -> llvm ir -> object code
Поправил.
> Охуительно. Толку от верифицированного кода, который проходит через все эти фазы трансляции, обогащаясь низкоуровневыми багами и даже логическими ошибками?
Тогда так:
idris -> c -> compcert -> object code. Я думал, тебе именно LLVM нужен, а если просто чтобы было, то пикрелейтед. Опять же, надо пынимать, что Идрис это во многом полигон для обкатки вещей, в программировании общего назначения принципиально новых. Там вон у самого Брэди ошибки при установке, сам себе issues открывает один за одним. Ты хочешь чтобы снихуя все сразу работало, так не бывает. Авиация началась с того что братья Райт на своем поделии три метра пролетели. Ну и там есть механизм запиливания собственных бэкендов.
Делают же люди дома из спичек, яхты в бутылках, модели Звезды Смерти, годами. А это чем хуже? Еще элитнее же выходит, не для быдла - должно быть привлекательно.
Популярность все это действо в целом какую-то имеет. Уже лет 20, если не 30, существуют норм пруверы. Постоянно делаются новые тулзы.
Даже ИТТ видно, что формальные методы привлекательны для некоторой прослойки задротов.
А самих доказательств, если рассматривать сложные теоремы за пределами школьного курса - пересчитать по пальцам одной руки старого фрезеровщика. Никто не копается углубленно, получается. Так, поверхностно поиграют с системой, и бросают. Недаром ИТТ (или в прошлом треде, не помню) большая часть постов была про установку и настройку редактора, лол. Такое впечатление, что на этом все и заканчивается.
А там правда нужно прям знать математику? Если доказательство уже расписано где-то словами, то мне кажется больше инженерная, механическая работа. Раскопать определения, записать их на формальном языке, заполнить пробелы в доказательствах, закодить какие-то стандартные приемы. Ну то есть знать на университетском уровне надо, конечно, но прям чтобы математиком быть - сомневаюсь.
>то доказывать будешь школьное говно.
А мне норм.
Кстати, чому пруверам на учат в школе?
>Наш язык для просветленных социалистов, а не потребителей
>средний школьник (АУЕ быдлан с потухшими глазами и гниющими от крокодила руками, из математики с трудом освоивший только сложение на пальцах в 15 лет)
Я имел в виду не ебеня Казахстана, а нормальные ДС-школы, не обязательно 57, но что-то более-менее приличное.
Нахуй вы это говно учите?
Спрошу тут. А почему программирование не пошло по такому пути? Ну скажем, описываем на некоем языке регистры процессора. Также описываем действия - то есть по сути регистры до, действие, регистры после. (Не только регистры, но и флаги, память, не суть). Потом описываем что должна делать программа (например вывести число на экран). А компьютер уже сам подбирает алгоритм, исходя из того что мы хотим получить (возможно мы задаем хинты, что важнее память или производительность, хотя по идее и это он сам может шедулить). Сам подбирает нужные команды процессора. Какие подводные камни?
То есть описывать не последовательность действий (императивное программирование), а результат (декларативное)?
На практике получается, что результат надо описывать слишком подробно, потому что его надо декомпозировать на подрезультаты, которые, по сути, являются подздадачами, и в конце получается точно такой же императивный код, но вывернутый наизнанку.
Можно сравнить с рецептом, как я писал здесь >>1685842 →
У борщехлёбов другое мнение, но кого оно волнует.
Ну как он это сделает? Это всего лишь машина, которая не может сама думать и не может магически влезть в голову программиста, чтоьы понять, чего он хочет. Единственный способ - обернуть простейшие команды в более сложные, их ещё в более сложные, и так далее до привычных процедур. Всё, что можно сделать - немного изменить семантику на самом верхнем уровне, но под капотом будет то же самое.
>>1748451
В тот раз внятных аргументов, кроме РЯЯ ВРЁТИ, я так и не услышал, уверен, что не услышу и сейчас. Поэтому уходи.
Шо тут непонятного то? Программист задекларирует, например, что есть команда копировать файл. Опишет что вот у нас диск до выполнения команды, а после выполнения команды диск должен содержать дополнительную копию указанного файла. Что тут мешает компьютеру самому определить, какие действия надо провести, чтобы получить желаемое изменение?
По сути, компилятор для всего. Ведь это то же самое, что делает компилятор, когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение, разве нет?
Не совсем понятно, как это должно выглядеть. Так что ли?
исходное_состояние = [файл, ⚹]
прочее = исходное_состояние - файл
новое_состояние = [файл, файл, прочее]
эвм.начать_думать(исходное_состояние, новое_состояние)
Чем-то напоминает пролог. Ты не на него намекаешь? Деталей я не знаю, но, вроде, выяснилось, что он оказался не всесильным и слишком сложным для чего-то реального.
> когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение
Это оптимизация, а не игра в угадайку. Изначально никаких оптимизаций не задумывалось, предполагалось, что как пишет программист, такие инструкции и будут. Оптимизации же появились не чтобы решать задачи за программиста, а чтобы прозрачно для него ускорить работу выполнения кода.
> регистры до, действие, регистры после.
>>1748240
>>1748440
>>1748535
Хуя тут авангард мысли. Так и до логики Хоара додумаетесь, а может быть даже и до separation logic. Между прочим, программирование в стиле "дать комплюхтеру задачу, а он пусть сам ебется с ее реализацией", это ровно то, чем занимается например Брэди сотоварищи в рамках type-driven development. Но там пока все очень далеко от идеала, уточнять постановку задачи по ходу дела должен таки человек. К этому же в идрисе столько всяких кодгенов, во втором идрисе, например, третьего дня кодген js запилили. Т.е ты делаешь на идрисе чего тебе надо, а потом компилишь всю хуйню в жс итд.
> прувер для metamath
HoTT бы автоматизировали, а метамат этот кому нужен? Там и нейроночки не нужны, записать его в BNF форме и генетические алгоритмы прикрутить, которые к слову, превосходят deepRL в играх атари, грамматической эволюции там более чем достаточно.
Автоматизация доказательств не имеет смысла.
В программировании, даже если код суперуёбищный до такой степени, что никто не понимает как он работает - он всё равно выполняет какую-то функцию, он полезен.
А в математике блекбокс прувер который отвечает да/нет как раз не имеет никакой пользы, потому что в математике важнее "каким образом", "что это значит" и "что это нам даёт", а на такие вопросы манясетки конечно же не ответят, пока что их удел - разгадывать капчу.
> Автоматизация доказательств не имеет смысла.
Сказал зумер. Судя по написанному дальше, вообще не понимающий о чем пишет.
кто теперь агдоводы?
классика ("моя голубка, мой голубочек"): https://www.youtube.com/watch?v=csgz5x8TYws
(записывает в блокнотик)
на третий день обсервации госпитализированный пациент продолжает идентифицировать себя с домашней птицей французской породы.
от предложенных рыбных блюд отказался, обосновав это своими сексуальными проблемами.
рекомендации: продолжать наблюдение.
(энциклопедия метро)
Какая тогда принципиальная разница между верифицированным автоматически доказательством и обычным, проверенным вручную?
Машина ошибается гораздо реже чем человек, и чем сложнее задача, тем больше вероятность ошибка человека. Например попробуй перемножь две матрицы хотя бы 10 на 10 вручную, с огромной вероятностью ты допустишь много ошибок, в то же время компьютер их перемножит за долю секунды абсолютно правильно.
Так Idris же вроде язык общего назначения, с элементами прувера.
https://arxiv.org/abs/2004.13472
"The categorical model of the quantum circuit description language Proto-Quipper-M... and provide them with operational semantics as well as a prototype implementation"
Ты про DALL-E? Он также работает в связке с GPT-3. Сейчас возможности GPT-3 по программированию ограниченны, но это только потому что в датасет не были включены сорсы из гитхаба. Как только будет выкачен GPT-4 (надеюсь, с гитхабом), GPT-3 станет не просто мощнейшим инструментом программиста, он сможет заменить его end-to-end в большинстве задач, связанных с айти: написание сайтика, поиск багов, тайпчекинг, написание компиляторов, любых программ, на любом языке программирования. И кроме всего прочего, сделает тебе красивую md-документацию для сгенерированного кода.
Мы на пороге революции.
>>1905928
Ты не понимаешь, о чем пишешь. 1+1=2 безотносительно того, отключат свет или нет. То же самое с любыми правилами построения в прувере. А вот горький петух со своим форсом гпт3+ вполне может оказаться прав, итеративный файнтюнинг таких нейроночек + внешние средства проверки правильности типа того же прувера, могут реально толкнуть вперёд всю эту тему настолько, что свидетелям эйдосов и "превосходства человека над бездушной машиной" может реально поплохеть от возможностей автоматизированного доказательства. Не будем забывать, что по-сути, простой брутфорс обьебал в шахматы Каспарова ещё в 1997 году.
>А это и есть высокое
>Куда тебе до высокого
ваш "ИИ" пузырь раздули инвесторы всего несколько лет назад.
еще через пару лет инвесторы выйдут со своими деньгами (иначе зачем они заходили), а бывшие МЛ-стартаперы побегут за новым хайпом хвалить что-то новое "высокое".
прогресс не остановить
40 лет назад пруверы работали кое-как и велись исследования
в наши дни пруверы работают кое-как и ведутся исследования
и еще через 40 лет пруверы будут работать кое-как и еще активнее будут вестись исследования
потому что пруверы - это о высоком
это компутер сайенс и рисёрч, а ваши вшивые стартапы
это прогресс
Бля, нам один препод в течение нескольких курсов давал один и тот же курсач, где надо было в ебучем экселе построить модель со сложной статистикой, и мы там юзали огромные формулы со всякими ДВССЫЛ и СЦЕПИТЬ, графики, сводные таблицы, фильтры, сортироввки, охуеть вообще.
только самое веселое началось по телевизору, как сразу "детям пора спать".
где вы видели незаконный прувер?
это вам не статические анализаторы или инструменты фаззинга, тут все тихо и академично.
на Ada+Spark летают ракеты, но это никого не интересует, это и так все знают.
Написал hello world и калькулятор, — вот и молодец. На этом стоп. Не стоит вскрывать эти конпеляторы и гитхабы. Это тебе не колидоры вычистлительных центров НАСА, даже не датацентры ГУГОЛ, не уютненькие офисы ФЕЙСБУКА. В сферу IT лучше не лезть. Серьезно, любой из вас будет жалеть. Лучше закройте Хабрахабр и забудьте, что тут писалось. Это все вранье, чтобы привлечь как можно больше новых макак на рабочие места и создать демпинг зарплат. Я вполне понимаю, что данным сообщением вызову дополнительный интерес у воротил из Cisco, SAP и IBM, но хочу сразу предостеречь пытливых — стоп. Зарплаты у IT-шников очень унылые. Остальным их просто не дают.
>>1512674 (OP)
>Это — борда для обсуждения ковариантных функторов, анафорических макросов, пандорических захватов, кластеров метапарадигм, катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов, ненужности математики, наконец.
>ненужности математики
Ахаха. А математике твои пруверы нахер не нужны.
И что теперь?
Даже тред в /pr запилили, а не в /math, наверное, потому что там уже есть загон для подобных шизиков в оснований-тредах.
я даже это не осилил
Вот есть типа книги по математики там. И там теоремы всякие. Они доказываются как на картинке и их никто не проверяет, просто люди от балды лепят себе звания академиков там всяких.
И пошла идея, что надо, чтобы компьютер доказывал так как он не особо может давить авторитетом. Пока что не очень получается так как давление авторитетом всё же происходит через непонятный синтаксис с кучами страшным значков.
А доказательство это типа про типизацию.
>кроме меня тут с верификацией кода вообще никто не сталкивался
Наверное.
>на примере кока и уже упоминавшегося мной VST с написанным для него верифицированным подмножеством С
А что даст полная верификация всего С?
Любая программа на верифицированном С будет верифицированной?
Я не шарю.
>Я не перестал считать это направление путем в никуда, но как введение в предмет - вполне годно.
Почему это путь в никуда?
>>1953400
"простите, плохое воспитание"
https://www.youtube.com/watch?v=IPNu6ybSHuU
> Любая программа на верифицированном С будет верифицированной?
Да. Но его полностью верифицировать невозможно, хотя теми чуваками верифицирована бОльшая часть.
> Почему это путь в никуда?
Потому что С не про верификацию, его создавали без учёта таких возможностей, это уже недавно придумали. Как я говорил выше, правильный путь - изначально верифицированный код. И лучший вариант это написание кода на чем-то одном, а затем его компиляция кодгенами во что угодно, как и работает Идрис 2.
>>1953400
> Но я так и не понял, это путь в никуда, потому что полная верификация ничего не даст, или полная верификация - это путь в никуда?
Полная верификация С невозможна, что доказал Аппель сотоварищи. А та часть, которая таки верифицируема, ее намного проще генерировать кодгеном в идрисе.
> > Любая программа на верифицированном С будет верифицированной?
> Да.
Для того, чтобы программа на С была верифицирована, ей же нужна спецификация, не? Т.е. любую программу на С надо или переписывать, или дописывать. Без спек, можно доказать отсутствие UB, "корректность" работы с памятью и проч.
Что я не так понимаю?
мимо пятую книгу не читал
Возможно ли теоретически построение верификатора, верифицирующего самого себя?
Или это алгоритмически неразрешимая задача?
>>1954358
> Теорема Геделя в помощь.
Педеля. Не знаешь - не неси хуйни. https://github.com/coq-contribs/coq-in-coq
> А потом вдруг выясняется, что система типов такая, что можно доказать Bottom. BINGO! Потом ее пофиксили, а через год опять нашли новый Bottom. А через год опять. Bottom - это полная жопа, никто не застрахован.
Бред какой-то. Почитай хоть, что это вообще такое. Какой ещё "новый bottom"? То Геделя приплетут, то вообще ШУЕ ППШ какое-то.
>Парни, а о чем тред?
Обколются своими пруверами, а потом сидят со стеклянным взглядом, исполняя странные пассы руками.
https://www.youtube.com/watch?v=w-HuQun8Cgc
>Сынок, ты не понял.
https://quran-online.ru/54:1
>борда
https://fr.wikipedia.org/wiki/Jean-Charles_de_Borda
>ковариантных функторов
https://en.wikipedia.org/wiki/Functor#Covariance_and_contravariance
>пандорический захват
https://letoverlambda.com/textmode.cl/guest/chap6.html
>анафорических макросов
https://en.wikipedia.org/wiki/Anaphoric_macro
>кластеры метапарадигм
https://www.biorxiv.org/content/10.1101/818948v1.full (?)
>катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов
https://github.com/hemanth/functional-programming-jargon#morphism
>слесарские проблемы
https://arhivach.net/thread/36498/
> Ваш жалкий практический земной мирок не нужен.
https://www.google.com/search?q="Ваш+жалкий+практический+земной+мирок+не+нужен"
Человек-мем.
Во второй U : U, например.
https://github.com/idris-lang/Idris2
>Things still missing
>Cumulativity (so we currently have Type : Type! Bear that in mind when you think you've proved something :))
> Better inference. Holes are global to a source file, rather than local to a definition, meaning that some holes can be left in function types to be inferred by the type checker. This also gives better inference for the types of case expressions, and means fewer annotations are needed in interface declarations.
Автозаполнение дыр теперь работает на уровне всего кода.
>>2014660
> Holes are global to a source file, rather than local to a definition, meaning that some holes can be left in function types to be inferred by the type checker.
То есть, при правильной организации кода, тайпчекер сам почти все напишет за тебя. Ставишь задачу, импортируешь нужные модули, расставляешь дыры (что нужно дописать) и тайпчекер сам их заполняет. Потом просто кодгеном получаешь исходник на нужном яп, причем, это гарантированно корректный код. Type-driving development это реально будущее программирования. Лямбды только сейчас завозят в мейнстримные параши, лет через 30 то что уже сейчас может Идрис2, завезут в мейнстрим.
> Может и есть за меня будет?
Поридж? Да нет, это для таких как ты только
Во-первых, ты путаешь тёплое с мягким.
>почему программирование не пошло по такому пути?
По пути использования пруверов в качестве языков для написания программ? А ты сам пробывал писать динамические опердени на Агде? Это чудовищно трудозатратно. Я даже видел где-то какой-то анализ производительности программистов. Было что-то вроде, что пищут сотни строк на Джаве, а на французком Петухе или на шведской Курочке средняя производительность программиста - 3 строчки кода в час. Сейчас не найду уже.
Чем больше инфы ты запихиваешь в статическую аппроксимацию поведения программы (т.е. в типы), тем больше усилий надо приложить, чтобы выполнить формальные требования тайпчекера и доказать, что даже самая элементарная программа работает корректно.
И это нихуя не про автоматизацию. Даже в банальной System F вывод типов неразрешим. Это не про автоматизацию, а про то, что ты почти вручную в рамках какой-либо логики доказываешь корректность программы.
И это не даёт особых преимуществ. Людям нужны программы, которые стоят дешево, быстро создаются и работают быстро. Можно въебать охуллионы шекелей в доказательство полной корректности HelloWorld, но если Call of Duty, написанный на С++, работает более-менее нормально и еще там есть графоний, то какая нахуй Агда? Тестировать банально дешевле, чем доказывать. Ну там в каких-то очень специальных случаях хочется иметь формально верифицированное ядро, но это именно что очень специальные случаи, а не программирование общего назначения.
>...
То что ты описал дальше - это использование декларативных языков и автоматических оптимизаций. Это ортогонально пруверам. Декларативные языки есть, и они очень успешны в своих сферах. Тот же SQL. Дальше ты вообще описываешь банальные оптимизации, вроде раскраски регистров и подбора оптимальной последовательности команд, что делает вообще любой современный оптимизирующий конпелятор. Это не имеет никакого отношения к формальной верификации программ.
Да, конпелятор Курочки, или того-же Хаскеля, теоретически может забабахать больше оптимизаций. Т.к. он имеет больше статической информации о программе. Следовательно, у него больше вариантов в плане выбора альтернативных последовательностей инструкций, которые приведут к тому же результату. Но, на практике, тот же JavaScript оптимизируется вполне сносно. А С++, при наличии более-менее прямых рук, никакой Хаскель, а уж тем более Курица или Петух, никогда даже близко не догонят. Я уж не говорю про то, что быдлокодера на С++ гораздо проще подготовить, чем спеца по Курице.
> И это нихуя не про автоматизацию. Даже в банальной System F вывод типов неразрешим
Что вы все в эту неразрешимость вывода типов упёрлись? Property-based testing делает вжжж и всё. Quickcheck'у больше 20 лет уже. Если кому-то надо разрешимый вывод для любой системы типов, с нынешними вычислительными мощностями это очень условная проблема.
> Курица или Петух, никогда даже близко не догонят.
Они и не для этого вообще-то. Даже Идрис это больше испытательный полигон для методов, которые завезут в мейнстрим.
>>1512715
> >Прувер
> О чем тред?
Поддвачну вопрос.
Об автоматическом доказательстве теорем. Записываешь теорему с определениями на неком формальном языке, понятном пруверу, а он говорит, долбоёб ты или нет. Правда, ни один анон в этом треде дальше школьного говна по алгебре не продвинулся. Интереса к хуйне без задач мало, почти за два года бамплимит не был достигнут.
Я видел MS сильно дрочит на доказательства https://project-everest.github.io/ , ещё видел ats. Это же рилейтед, т.к. идрис и lean4 в шапке. spark же взлетел.
Причем тут Property-based testing? Разрешимость даёт мне то, что я просто пишу код, а конпелятор сам его проверяет. Неразрещимость означает, что я должен какие-то типы сам в голове вычислить и конпеляту указать, чтобы программа прошла тайпчекер. Причем тут вычислительные мощности? Неразрешимость означает что у уравнения в принципе нет решения, какие бы вычислительные мощности там ни были. Нужно руками всё делать, без комплюктера.
Ты не понимаешь смысла неразрешимости вывода типов в какой-то теории типов. Не надо это путать с неразрешимой в принципе задачей.
> . Неразрещимость означает, что я должен какие-то типы сам в голове вычислить и конпеляту указать, чтобы программа прошла тайпчекер.
Вера швятая во магическую "вычислимость в голове", чем-то отличающуюся от вычислимости в общечеловеческом смысле.
Он не может. Во-первых, этот анон имеет очень хуевое представление о чем он пишет, потому что он нахвался хуев по верхам в понве и смежных с ним раковниках. Во-вторых, это крайне абстрактная хуета и бытовым языком не излагается. Но это ничего, потому что применимость у нее околонулевая, и если бы не попил грантов - была бы нулевая.
> он нахвался хуев по верхам в понве и смежных с ним раковниках
Я даже не знаю, что это такое.
> Но это ничего, потому что применимость у нее околонулевая, и если бы не попил грантов - была бы нулевая.
Ну раз так сказал зумер с лгбт-пельменницей симплдимплом / попитом наперевес, наверное так оно и есть...
>>2057102
Поридж, хоспаде... Теорема записывается в виде типизации. Если теорема верна, она соответствует непустому типу, если неверна - пустому. Ну и ещё есть вариант с потенциально бесконечными типами.
Если брать Lean 3, то там quotient types вместо setoid hell’а (с другой стороны, это ломает хорошее свойство: в Lean не любой закрытый терм, принадлежащий определённому индуктивному типу, приводится к виду, состоящему из его конструкторов; с другой стороны, в Lean community много модульных дедов, что ебашат везде noncomputable, которым на вычислительные свойства похуй, поэтому это никого особо не волнует); синтаксис поприятнее (ИМХО) с человеческой поддержкой юникода; вместо отдельного языка для тактик сам Lean (в виде meta‐кода); плагины что для Emacs’а, что для VSCode чекают код на лету; более‐менее нормальный IO из коробки.
В Lean 4 к этому всему добавляется хорошо расширяемый синтаксис (см., например, https://github.com/leanprover/lean4/blob/master/tests/playground/forthelean/ForTheLean/Demo.lean#L75).
> Lean
Да ненужен он. Полноценные пруверы это кок и агда. Для агды весьма активно пилится категорная либа, agda-categories, можно опучкаться если кому надо. Есть попытки упростить прувер до плагина к редактору кода - arend, он ещё и на основе HoTT. Для верифицированного софта есть Идрис2 и соответствующая парадигма программирования - type-driven development. А этот ваш Lean хз для чего и кого
- Все термы в coic имеют вычислительный смысл, это не религия в которую надобно веровать
- Какой тогда вычислительный смысл у конструктора (индуктивного типа)?
- Он тривиальный
(из бесед с конструктивным петухом)
- Лямбада исчисление абсолютно, идеально, на нем будут писать инопланетяне, можно сказать что это Язык Бога
- А что вы скажете по поводу других вычислительных формализмов?
- Ну они тоже в принципе ничего
(из интервью Вадлера)
- В теории типов все правила интродакшена и илиминейшона идеально сбалансированы, это имеет глубокий вычислительный смысл
- Вот true терм, вот его интродакшен, илиминейшона нет - потому что не нужно
(с лекции Харпера про HoTT)
Скажите, имеет ли смысл вкатываться в эти ваши пруверы для лучшего понимания математики?
Если я, например, не пониманию логику доказательства теоремы, могу ли я переписать ее в код и посмотреть как это пошагово происходит? Покажет ли мне софтина промежуточные этапы?
Правильный путь воина примерно таков:
почитать про metamath
разобраться с доказательством 2+2=4
написать интерпретатор mm
создать систему под себя с нужными тебе аксиомами и правилами вывода
доказывать то что тебе интересно в ней
(опционально можно metamath на hol заменить)
С другой стороны если ты не можешь создать такую систему которая механически
подтверждает твои выкладки можно ли вообще говорить о наличии понимания того
что ты делаешь?
>Покажет ли мне софтина промежуточные этапы?
Покажет, только они будут настолько тривиальными и их будет настолько много, что ты не сможешь ничего прочитать. По тем же причинам, по которым не можешь понимать программы в байткоде.
>>2079468
Спасибо за инфу, аноны.
В общем, насколько я понял, это всё не совсем то, что мне нужно.
Все эти метаматематики объясняют сложное с помощью еще более сложных и упоротых слоев абстракции.
Мне же нужно нечто совсем другое.
Чтобы было возможно посмотреть на обычное доказательство, но так сказать интерактивно, в процессе. Есть ли вообще такое?
> anonymous function
Это же лямбды, они везде примерно такого синтаксиса. Разница между тем, что на твоём пике, и скажем тем что в коке или агде в том, что в последних типизированная лямбда, т.е для всех термов нужно указать ещё и тип. Всё, остальное ровно так же. Типизированная лямбда даёт гораздо больше возможностей.
>>2084830
> Зачем нужны зависимые типы, когда есть тройки Хоара? Я бы вообще выкинул из языков все типы, как в Питоне, и оставил бы только тройки Хоара. Почему так не сделают?
Затем, что при сколько-нибудь сложном выражении тройка Хоара {P} c {Q} требует полного пересчитывания всех термов, а это не только >99% бесполезного труда, но и не всегда возможно. Есть более продвинутый вариант троек Хоара - separation logic, где считаются только непосредственные изменения, но и они нахуй не нужны, ибо сводятся всего лишь к зависимому сигма-типу. То есть, твое предложение сводится к тому, чтобы заменить все зависимые типы на один сигма-тип. Сделать это можно, но в итоге это приведет к выбрасыванию на помойку 90% возможностей зависимых типов.
> Все эти метаматематики объясняют сложное с помощью еще более сложных и упоротых слоев абстракции.
> Мне же нужно нечто совсем другое.
> Чтобы было возможно посмотреть на обычное доказательство, но так сказать интерактивно, в процессе. Есть ли вообще такое?
Тактики в коке разве что. Там весь процесс доказательства можно вывести пошагово.
Есть HIT в Агде (с кубиками)
data UList {a} (A : Set a) : Set a where
[] : UList A
_∷_ : A → UList A → UList A
∷-comm : (x y : A) → (xs : UList A) → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
trunc : isSet (UList A)
и функция
length : ∀ {a} {A : Set a} → UList A → ℕ
length [] = 0
length (x ∷ xs) = 1 + length xs
length (∷-comm x y xs i) = suc (suc (length xs))
length (trunc xs ys p q i j) = ?
как сделать чтобы функция работала с последним случаем?
пробовал "(cong (cong length) (trunc xs ys p q)) i j", но не проходит termination checker