>Прувер
О чем тред?
На этом вашем Петухе хотя бы интернет-магаз то реально написать, или очередной высер без задач?
>интернет-магаз
Наш язык для просветленных социалистов, а не потребителей
Сынок, ты не понял. Это — борда для обсуждения ковариантных функторов, анафорических макросов, пандорических захватов, кластеров метапарадигм, катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов, ненужности математики, наконец. Никого здесь твои слесарские проблемы не волнуют. Ваш жалкий практический земной мирок не нужен. Съеби.
Что за псевдонаучные термины? Что-то из вашего очередного брейнфака?
>социалистов
*Борщехлебов
Поправил тебя
А я говорил что ФП это марксизм
ОП, ты таблетки принял?
Зачем ты такие треды создаешь в белом интернете, это незаконно вообще то.
Зачем ты такие треды создаешь в белом интернете, это незаконно вообще то.
Да в /pr все вне закона, кроме вкатывальщиков.
И зачем? Тут никто ничего нового и не прочитал ещё. Приходи через пару лет.
СОQ тьюринг полный, можно написать всё что угодно.
Можно написать интернет магаз из которого гарантированно нельзя украсть деньги. Только писать нужно всё самому, начиная от сетевого стека и базы данных.
Если очень хочется, можно посмотреть на `coq.io`
Как доказать что функция тотальна, если кок не понимает, что я уменьшаю аргумент?
Ты выглядишь шарящим.
мимо
Очередной тред для пиара Максимки Сохацкого?
Да хоть в тапки ему нассать. Лучше пруфать научите.
На сосач, быдло!
На натуральных числах должен просто работать паттерн-матчинг.
Для остальных - хз.
Ну это только для снятия S работает. А вдруг я поделить и/или вычесть хочу. Он уже не понимает. Как подсказать то...
PS можно дополнительный аргумент протаскивать, но потом надо пруфать, что он на результат не влияет, а мне тяжело.
Именно.
В 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».)
Хватит заниматься этим фуфлом!
Это по любви. За остальное надо требовать деньги.
Зумера вкатывальщики не могут в пруверы по причине отсутствия мозгов. Но даже если зумер осилит кок, это не даст ему ничего, потому что он все равно не может в математику, т.е даже в элементарное практическое применение того же кока.
Оп, почему нет этого прувера https://arend-lang.github.io/ вроде интересная тема. Как минимум потому что там HoTT это основной язык, а не костыли над основным, как в коке или агде, ставится в полтора клика как плагин к IntelliJ, есть обзор на швабре https://m.habr.com/ru/company/JetBrains-education/blog/469569/
Да не гори, осилишь ты кок.
В голосину
Почему так мерзко от пика?
>почему нет
Предпоследняя ссылка в топике вообще‐то.
>а не костыли над основным, как в коке или агде
>агде
«agda --cubical» погугли.
> «agda --cubical» погугли.
Я это даже ставил. Отдельная либа же. Или что-то другое есть?
> Предпоследняя ссылка в топике вообще‐то.
Лол, в глаза долблюсь.
>Отдельная либа же.
Ну так там в ядро агдочки встроены кубические примитивы.
А ты случайно не в курсе, как Идрис поставить через stack, если его нет в stackage?
Не, я не пользуюсь ни шидрисом, ни stack’ом.
Как ты живёшь вообще?
Нормально живу.
А что с прошлым тредом? Неужели утонул? Какая жалость, кек.
Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
natU : ℕ → U
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
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
>аксиомы coic
Вот же дебил.
Первый верун порвался.
Что за система? Дерево вывода покажи с аксиомами.
>Arend background.png
\У \куска \говяхи \синтаксис \лучше
>Что за система?
Обычное MLTT, лол
> Дерево вывода покажи
А в чём разница? Всё понятно же, а в латех лезть мне лень.
Проебался, там вместо tr должно быть coe, но вы поняли.
Нет непоняли нихуя, ты шизик что ли реально что за tr coe ap ★ наконец?
> Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
То, что у тебя нет мозгов, потому что ты зумер, не значит, что их нет ни у кого.
Да нормальный синтаксис, быстро привыкаешь.
Проблема унивалентных оснований даже не в том, что эту тему по-сути 3.5 тела тащат типа Мортберга, ещё и Воеводский помер, пиздец. Главное - конструктивная математика изначально малопригодна для прямого использования людишками из-за сложности построений. Ещё Брауэр писал, что его интуиционизм без проблем можно использовать только при наличии бесконечной памяти, т.к манипуляции со сколько-нибудь сложными ментальными построениями требуют гораздо больше мозгов, чем их есть у кого угодно. В наше время половина этой задачи решена - кудахтеры + HoTT, в общем дают возможность доказать что угодно, любая математика представима в унивалентных основаниях. Однако, все это не отменяет того, что большую часть пруфов надо писать вручную. А в случае сложной матчасти и на это тоже мозгов не хватает ни у кого. Даже Мочидзука свою IUTeich в унивалентных основаниях переписать не осилит. Нужна автоматизация подобного рода пруфов, причем, одними тактиками это сделать не получится. Идеи есть, как это реализовать, но времени нет совсем. То одна хуйня, то другая...
#CHLOR НА ФРИНОДЕ #CHLOR НА ФРИНОДЕ О БОГИ ОДИННАДЦАТЬ ИЗ ДЕСЯТИ #CHLOR НА ФРИНОДЕ
НЕ РЕКЛАМА
НЕ РЕКЛАМА
НЕ РЕКЛАМА
#CHLOR НА ФРИНОДЕ
Серануть любой может, вот только доказательства все нет.
Ой дибил... дерево вывода где? Где аксиомы? Ты просто веруешь.
алсо
>То, что у тебя нет мозгов, потому что ты зумер
у убогих мандавошек проекции просто одна охуительнее другой.
>Проблема унивалентных оснований даже не в том
>можно использовать только при наличии бесконечной памяти
Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время". Хотя думаю нет - они ж были совсем не тупые как местная пидорва.
Вы даже хуже Rust-борщехлебов.
ты что дибил, дед? какие аксиомы? это ж чистое лямбда исчисление. тут только определение функции, аппликация, бета редукция и эта экспансия. Этого хватит чтобы доказать эту теорему.
>ты что дибил, дед? какие аксиомы? это ж чистое лямбда исчисление.
Совсем дурак шоле?
>тут только определение функции, аппликация, бета редукция и эта экспансия. Этого хватит чтобы доказать эту теорему.
Тут как минимум нужен ещё J для равенства пути
Нужно и равенство да, но если есть индуктивные типы для чистого исчисления (Cedile), то можно элиминаторы равенства и его бета (J) и эта правила (которое в не HoTT системах запрещено) написать в чистых функциях. Так то дед! Ты не совсем дибил если знаешь про J, но явно отстаешь от индустрии лет на 5.
Плюс в кубиках J дерайвабл, так что J уже давно ни у кого не аксиомах (как минимум в PTS CiC системах типа Formality и кубиках).
Ну вот мы и видим как еще один верун дристанул под себя. Естественно никакого дерева вывода можно не ждать, ведь ты не имеешь ни малейшего понятия как работает твоя система, а просто в нее веруешь.
>для чистого исчисления (Cedile)
>дает доказательство в lean
Максимальная маневренность. Хотя до чудика выше что дал доказательство в собственном маня-mltt еще далеко.
Ты просто ни разу NbE не написал и живешь в бумажных деревьях, математик которые не может в дебагере выставить printf будем вопить и плеваться на анонимных досках, потому что в то время пока он будет рисовать никому не нужную макулатуру на бумаге, программисты будут писать за него теоремы о неподвижной точке.
труси костями и ползи на кладбище со своими бумажками.
ты вообще никому нахуй не нужен, можешь только в подворотням недостудентам про матанализ рассказывать с голоду. Ты даже в автоматизации математики бесполезен!
Генценовские деревья выводов блядь он просит в третьем тысячилетии. Лол
Это просто Арнольд-2.
Ну давай показывай тогда как ты доказываешь зумерок
Я почитал все твои высеры на дваче, мистер Арнольд, перед свиньями бисер не бросаем, и вам не советуем. HoTT это секта не для челяди и совковых бумажных математиков.
Сри дальше, а я буду смотреть через сколько лет ты разовьешься хоть во что-то или так и будешь передавать знамя невежества своим сынам и воинам долбоебизма.
Подводим промежуточный итог:
Вопрос: докажите 0 ≠ 1.
Пруверо-пидорва: ссытся под себя и пускает слюни от собственной беспомощности.
Ясно.
Вопрос: докажите 0 ≠ 1.
Пруверо-пидорва: ссытся под себя и пускает слюни от собственной беспомощности.
Ясно.
У тебя ж два доказательства на руках, на Agda и на Lean. Или у тебя проблема какая-то в коммуникации и ты не можешь прочитать книжку и вместо своего СДВГ ты лезешь в интернет и орешь "это не доказательства!", "Арнольд говорил компьютеры не нужны!". К чему это все? Мы можем тебе написать доказательство 0!=1 на всех MLTT языках не вопрос. Но во-первых ты не принимаешь эти доказательства. Я слабо верю в то, что ты не веришь что существует изоморфизм между генценовскими палочками и трейсом работающей программы на компьютере. Ты либо просто ебанутый либо человек с нарушенными коммуникативными способностями.
>У тебя ж два доказательства на руках, на Agda и на Lean.
На агде можно вроде бы проще написать в одну строчку, за Lean-поебень не скажу. В коке я могу вообще одной командой это сделать - inversion - и готово, охуеть да как ловко? Только я спрашиваю на каких фундаментальных принципах основываются эти доказательства. Проблемы не с моими
>коммуникативными способностями
а только с мыслительными способностями местной пидорвы. Они даже не понимают о чем их спрашивают. "Ну раз система говорит что это так значит это так" - верунчики, что с них взять. Особо продвинутые еще могут про швятой изоморфизм спиздануть не к месту.
>ты не можешь прочитать книжку
>своего СДВГ
>Арнольд говорил компьютеры не нужны!
новые потешные проекции подоспели.
Ты ж великий бумажный математик, построй категориальную модель инфинити топоса, заэкстракть оттуда язык внутренней логики и получишь вычислительную модель ТС.
То он Арнольд, то воинствующий Кок-петушок уже.
Коком из математиков уже никто не пользуется, кстати, он годится и используется сейчас только для системного программирования и верификации. Даже конференций по Коку нет масштабных, а все авторы Кока ездят на Lean конференции и пишут на Lean.
А вот возьму и построю. Ты то что будешь делать, манька, так и будешь продолжать веровать и молиться швятому автоматону?
>То он Арнольд, то воинствующий Кок-петушок уже.
Манька запуталась в собственных маня-проекциях, так мило.
И что они там делают, рассказывают MS-блядям что уже есть система для нормальных людей? Накидай линков что ли.
Это чисто математические тусовки, там даже математиков с ноутами на винде нет. Это спонсируется грантами евросоюза. Ну если ты можешь построить Модельнеые категории для инфинити топоса на слабых расслоениях симплициальных множеств, то уже будешь 6-й в списке тех, кто это сделал.
Даже не 6-й, а 8-й уже.
Интересно как ты собрался строить это? На бумажке стрелочки рисовать будешь или пьесу в трех ролях разыграешь?
У Воеводского вон не получилось, у филдсовского лауреата то, я хочу посмотреть что ты высрешь!
> Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время".
Для их нотации время давно прошло. Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
Он же математик, это называется синтетическая теория, как аксиоматика Гильберта или Вейля. А так то клован, да :-) HoTT же тоже синтетическая теория. Давайте запутаем его!
>где аксиомы?
Аксиомы Lean?
https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf
>дерево вывода где?
Вон тебе бумажка, сам выписывай. Я ебал такой хуйнёй заниматься.
>Ты просто веруешь.
Верую во что?
В то, что авторы Lean действительно написали то, о чём рассказывает та бумажка? Да, верую, не разбираться же мне в тоннах крестокода.
В то, что существуют контексты и переменные? Да, верую, что тут такого?
В propext? Да, верую, но в чём проблема?
В choice? Если надо, тоже уверую.
До чего ты доебался, петух?
> Lean
Чем он вообще хорош? Когда-то это был первый прувер на основе HoTT, потом это выпилили.
Потому что ты видишь потреблядей, оболочек, а не духовноразвитых людейчтобы это не значило.
Нахуй это все нужно?
Если такие вопросы задаешь, значит тебе это точно не нужно.
Я и не собирался, просто хочу узнать зачем это вам.
Из особых фич: метапрограммирование разве что. Ну квошенты, хотя этим никого не удивишь.
Ещё IO сразу есть, а не как в коке.
Четвёртая версия в кресты компилируется (ещё обещают, что она будет ниибаца быстрая).
>Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
О, неужели конструктивный петушок показал свой клювик с подпевалами? Давай расскажи мне как конструктивная математика не нуждается в аксиомах потому шта она естественно правильна ведь там математики все делают на рефлексах и не могут ошибаться. А конпункторы у них хоть и рефлексов нет но они там что то вычисляют а раз оно что то там вычисляет значит у утверждения есть ВЫЧИСЛИТЕЛЬНЫЙ СМЫСЛ следовательно оно не может быть не верным. Как то так. Посмеши деда еще. Можешь про неформализуемость алгоритма ведь ТУЮРИНГ ПРОБЛЕМА ОСТАНОВА ГРОБ ЧЕРВЬ ПИДОР в своем манямирке спиздануть, очень потешно.
>Вон тебе бумажка, сам выписывай. Я ебал такой хуйнёй заниматься.
Боишься в 4,523,659,424,929 символов не уложиться что ли?
>До чего ты доебался, петух?
Хочу понять почему 0 ≠ 1, да что то рефлексов не хватает. Думал в этом треде мне смогут помочь ((((((
>Боишься в 4,523,659,424,929 символов не уложиться что ли?
А то.
>Хочу понять почему 0 ≠ 1
Бля, ну если ты этот пруф осилить не можешь, то земля тебе стекловатой, бро.
Что сказать-то хотел, чучело? Горелым пердаком по всему мейлру трясти у тебя время есть, а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету? Ну кукарекай дальше, если тебе это интереснее, чем хотя бы попытаться разобраться в теме, дело твое. Просто свое место у параши не забывай, твои победоносные кукареканья не делают тебя умнее создателей конструктивной математики, не забывай этот простой факт.
Как я его осилю если его тупо нет. Как можно осилить то чего нет? Местная пидорва все боится чего то обосраться и делает вид что лениво.
>НИПИЧОТ
Нормас петушка клинит. Главное не забудь на иконы Швятого Браузера и Мартина-Лефа перед сном передернуть.
>Как я его осилю если его тупо нет
Ты слишком жирный петушок.
> Посмеши деда
Говна на обед поел уже, дед?
Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
Запартная херня для дошколят.
>Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
Ты снова проецируешь, конструшила?
НИ ЕДИНОГО РАЗРЫВА АНУСА
Продолжай убеждать себя в этом конструшок.
Если кратко то Lean is a new Coq.
>МАМА У МЕНЯ ЖОПА НЕ ГОРИТ ПОВТОРЯЮ НЕ ГОРИТ
А если длинно?
>а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету?
Я кстати пытаюсь почитывать швятые писания, удерживая рвотные порывы, но таких "вершин" как конструктух мне никогда не достичь, потому что - паста
> понятно только ебанутым ... подобно тому, например, как христианам понятно как женщина была сделана из ребра мужчины, в то время как ни один нормальный человек такой хуйни никогда не поймёт просто потому что он нормален, а не ебанут
В чем цель всех этих твоих потуг, пидорша? Что и кому ты хочешь доказать?
Думал, что так просто натянуть на хуй программистов, но программисты оказались смышлёней него.
Если длинно, то Coq всегда был фреймворком для разработки тактик с удобным сопряжением со внешним миром. Lean в этом смысле более народный из-за С++ и в то же время более быстрый. В отличии от Coq, у Lean достаточно простое и понятное ядро, гораздо легче писать тактики, не нужно учить ocamlp5 и 4 промежуточных языка для этого. В Lean вкатаны уже достаточно интересные вещи типа перфектоид пространств, а все что вы можете найти на коке это либо старье либо как когда-то писали деды.
4-я версия Lean уже будет обладать макросистемой и self-hosting, поддерживать FFI в С/C++, можно будет писать свои веб сервера, консольные приложения, и проганять ваши теории на промышленных датасетах прямо в производстве на полях.
Тебе срачелу разворотить например. Вижу что результат весьма неплох.
Хороший самоподдув
>4-я версия Lean уже будет обладать макросистемой и self-hosting, поддерживать FFI в С/C++, можно будет писать свои веб сервера, консольные приложения, и проганять ваши теории на промышленных датасетах прямо в производстве на полях.
>СУПЕРКОМПЬЮТЕРЫ БУДУТ РАЗМЕРОМ С ТЕЛЕФОН, ТЕЛЕФОН С ИНТЕГРАЛЬНУЮ СХЕМУ, ИНТЕГРАЛЬНАЯ СХЕМА С НАНОРОБОТА, А НАНОРОБОТЫ В КАЖДОМ ПРЕДМЕТЕ БУДУТ СИДЕТЬ И ПЕРЕСТРАИВАТЬ МАТЕРИЮ НА СУБАТОМНОМ УРОВНЕ!
Ага и обратная совместимость по пизде пойдет и все
>интересные вещи типа перфектоид пространств
по пизде пойдут
>и в то же время более быстрый
Неужели прямо из MSR подвачевываешь? Мое почтение. Какой же невероятный пиздеж
>по пизде пойдут
Обещают режим совместимости со старым синтаксисом.
Да и всё равно перепишут.
Что, есть сомнения, что С++ тактики быстрее OCaml?
А что-нибудь типа quickchick планируется?
Кто-нибудь знает, x86 ISA верифицирована? Как там с доказанной корректностью процессоров, вообще?
Конечно все процессоры верифицированы уже.
486 верицифировали на ACL2, пентиумы уже на проприетарных чекерах.
Почему в верифицированной архитектуре могут возникать ошибки (как с FDIV в Пентиумах) или уязвимости как Meltdown или Spectre?
>проприетарных
То есть исходники закрыты? И как тогда проверить доказательство ИХ корректности?
А сами эти чекеры на x86 работают?
Будущее программного обеспечения это верифицированный софт и аппаратные средства. Представьте себе ИИ, недружественный к людишкам. Он без проблем найдет миллионы дыр в поделиях от индусских соевых анальников. И все, пизда. Единственный выход - сворачивать все эти хипстерские яп, разгонять ссаными тряпками дармоедов с петушиными андеркатами из барбишопа, всех этих зумеров вкатывальщиков и прочее быдло.
>маняфантазии борщехлёба
Дефект по типу «второй жизни» определяется тотальными странностями, распространяющимися на все сферы психической деятельности: эксцентричность внешности и речи, парадоксальность и дефицитарность эмоциональной сферы, достигающие степени регрессивной синтонности отношения с окружающими, полностью замещающие профессиональную деятельность аутистические сверхценные увлечения, – и сочетается с психопатоподобными расстройствами иного круга (зависимые, истерические) и псевдоорганическими/астеническими нарушениями.
При этом происходит переосмысление и ревизия системы ценностей, прежде всего относящихся к конвенциональной деятельности: прежние, социально значимые интересы (учеба/работа) отчуждаются и обесцениваются, подменяясь патологическими сверхценными увлечениями
Основным содержанием жизни (сверхценное мировоззрение при изменениях типа фершробен [Аведисова А.С., 1988; Birnbaum K., 1906]), становятся «патологические сверхценные увлечения» [Сергеев И.И., Малиночка С.А., 2008] с идеями реформаторства или собирательства – странные, оторванные от реальности хобби, выступающие в качестве проявлений односторонней аутистической активности и носящие характер необычных, подчас лишенных всякого смысла, не приносящих дохода увлечений
У борщехлебов очевидный фершробен, лол.
Аутизм - чек, нездоровые отношения с коллегами - чек, двойная жизнь - чек. В жизни это крудошлеп, боящийся сокращения, который 24/7 разгребает таски, а на двачах это успешный технофилософ каратель анальников.
Аутизм - чек, нездоровые отношения с коллегами - чек, двойная жизнь - чек. В жизни это крудошлеп, боящийся сокращения, который 24/7 разгребает таски, а на двачах это успешный технофилософ каратель анальников.
>Дерево вывода покажи
И покрути
Проиграл
>Да нормальный синтаксис, быстро привыкаешь.
В dlang скобки шаблонов <> даже выкинули чтобы лишний раз не заставлять шифт нажимать, а ты в 2019 предлагаешь такое нормой
Такое можно про любого увлеченного человека сказать. Охуеть, наука уровня астрологии.
Оба языка считаются "быстрыми", так что все зависит от криворукости писавших. Можно даже допустить что что-то там на lean работает быстрее и какое-нибудь мега-доказательство будет верифицироваться на lean всего два машино-месяца вместо четырех на coq. Вот только мне от этого совсем не легче когда я запускаю lean и оно у меня моментально отжирает гигабайты памяти, грузит проц на все сто и падает.
>Малиночка
хех ну вы лалки
Зачем для набора «\» шифт?
Почему тебе лень нажать шифт?
Начинать все ключевые слова с какого-то спецсимвола это и правда не от мира сего решение. Видно, что умы авторов языка пребывают в каком-то астрале, слабо связанным с такими земными вещами, как клавиатуры, глаза, эстетика.
>Начинать все ключевые слова с какого-то спецсимвола
В чём проблема‐то? Это расширяет диапазон допустимых имён для определений. В лишпе вон скобка на скобке, но никто не кукарекает, что это не от мира сего язык.
кукарекают кукарекают
>В лишпе вон скобка на скобке, но никто не кукарекает, что это не от мира сего язык.
Ессно - лисп мёртв, его дрочат два с половиной ебаната
Язык APL вообще специальную клавиатуру требовал
> Видно, что умы авторов языка пребывают в каком-то астрале, слабо связанным с такими земными вещами, как клавиатуры, глаза, эстетика.
Суть этих языков не в том, чтобы наиндусить как можно больше говнокода. Задача нотации - быть максимально прозрачной и близкой к общепринятой математической, для чего в той же агде поддержка юникода https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html
ну этот бекслеш в кубике джетбрейнса по началу тоже заебывал, но потом привык. Если Кнуту можно в TeX то и Исаеву тоже!
>Суть этих языков не в том, чтобы наиндусить как можно больше говнокода.
Так и про брейнфак можно сказать.
>Задача нотации - быть максимально прозрачной и близкой к общепринятой математической
И как в этом помогает \where?
Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Что значит «слишком сложен»? Я привел характеристики языков по значимому для меня набору критериев. Я осознаю, что существуют безмозглые пидоры, у которых в список значимых кримериев может входить, к примеру, синтаксис языка. Hу так накласть мне на них. Меня интересуют объективные критерии, а не цацки всякие.
(с) vsl
>Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Просто два чая этому любителю прекрасного.
Бамп.
Предновогодний бамп.
Вроде бы скрываешь треды, а через некоторое время, когда они почти утонули, кто-то их бампает, и они опять появляются. Почему так?
Потому что ты хуй, а это лучший тред во всем /pr/
Настолько лучший, что его даже бампать бесполезно?
Элитный, хули.
https://github.com/ice1000
Что это за азиатский монстр? Как столько всего можно знать в 19 лет? В 16, судя по коммитам он уже спокойно вертел avl деревья, пилил свои компиляторы и свободно владел парой десятков языках, ТК он также отлично знает, а сейчас устроился на позицию пруф чекера в жидбрейнс. Он гений или просто убер-задрот? Или всё вместе?
Что это за азиатский монстр? Как столько всего можно знать в 19 лет? В 16, судя по коммитам он уже спокойно вертел avl деревья, пилил свои компиляторы и свободно владел парой десятков языках, ТК он также отлично знает, а сейчас устроился на позицию пруф чекера в жидбрейнс. Он гений или просто убер-задрот? Или всё вместе?
Поправка: не теорем пруфера, а разработчика тулзов для теорем пруферов. Наверное доведёт arend до ума.
Если несколько лет дрочить все это по 6 часов в день, вместо хождения в говновуз, сидя на шее у родителей, то почему нет.
Олсо, где ты там его возраст нашел?
Потому что
нормальный штрих, урененный средний уровень хорошего мирового инженера!
Поясните за Идрис, подходит ли для прикладного программирования, или если не теорем пруверами заниматься то лучше не лезть?
> подходит ли для прикладного программирования
Нет. /thread
>прикладного программирования
Ты ещё заработать предложи.
Идрис говно из жопы, бери Агдочьку
согласен со всеми господинами!
Сереженька, бегом на кухню! Я борщик приготовила вкусный! Щавлевый!
А какая практическая польза ото всего этого?
Какие ссаные тряпки надо сувать в ОП-пост, чтобы вас тут не было?
Достаточно прекратить страдать бесполезной хуйнёй, а в кои-то веки выучить пхп и жс.
Те, которые ты намотал на себя
Зачем? У нас есть jscoq!
Если будет oraclecoq, то я с вами крч.
вообще-то пруверы в ИТ притащили именно для того, чтобы не получались такие поеботы как Ораклы больше никогда в индустрии.
>Haskell
>classless
Это другие, неправильные классы.
Ты слишком серьёзен. Лучше б что-нибудь доказал
> vs
Будто у них что-то общее, кроме названия.
Зачем вы это учите?
Мне сказали, что это филиал асилума а ты тут главный петух-газонюх.
Попукал вам в тред.
Бамп.
Чо скажете за dafny?
Это же refinement types, то есть не прувер.
Зачем тебе эта хуйня без практических задач, лучше питон возьми.
Держать питон прикольно первые десять минут.
Кто с TLA+ имел дело?
Toolbox медленный и работает коряво, например иногда курсор перескакивает куда попало, что меня несколько раздражает — есть ли ему достойные альтернативы?
Toolbox медленный и работает коряво, например иногда курсор перескакивает куда попало, что меня несколько раздражает — есть ли ему достойные альтернативы?
Ну как в СССР. Были два класса, рабочие и бюрократы. Но это не считается, это другое)))
А ещё классы есть в шкалке. Возвращаешься иакой из шкалки и пишешь тайпклассы.
Хорошая шкалка.
Поясните за пруверы подробно человеку, который когда-то занимался математикой. Я правильно понял, что это просто движок, который умеет делать преобразования на языке мат.логики, и может размотать изначальное выражение и проверить, приходит ли оно к тому, что надо доказать? Хорошо, а насколько эти движки скилловые? В смысле, мат.логика - это далеко не все. В процессе доказательства привлекаются самые разнообразные методы, в том числе и прямые математические расчеты(выражения и их численные значения), и различные продвинутые методы, даже иногда графические. Я уже молчу о том, что эти движки нужно постоянно обновлять, поскольку постоянно придумываются новые методы и новые области математики. Та же теорема Ферма, доказанная через эллиптические кривые - никому ведь ранее даже в голову не приходило связать одно с другим.
Единственное что этот язык не может, это работу тебе дать)))
Работа есть, дело в другом: слишком большой порог вхождения и нужно разбираться буквально во всём в CS, что бы что-то делать полезное.
Ссаный тред подёнщиков, которым никогда не откроются тайны бездонного моря алгебраической геометрии.
Да
Зачем?
Чтобы доказать
Нахуй вы это учите?
Потому что нам никогда не откроются тайны бездонного моря алгебраической геометрии, а так хоть что-то.
> Я правильно понял, что это просто движок, который умеет делать преобразования на языке мат.логики, и может размотать изначальное выражение и проверить, приходит ли оно к тому, что надо доказать?
Как-то так, да. Ибо пикрелейтед.
> насколько эти движки скилловые? В смысле, мат.логика - это далеко не все.
Даже йогурты не все одинаково полезны, про матлогику и говорить нечего. Но касаемо HoTT и CuTT - это как раз правильное направление матлогики, про которую нельзя сказать, что она "далеко не все".
> В процессе доказательства привлекаются самые разнообразные методы, в том числе и прямые математические расчеты(выражения и их численные значения), и различные продвинутые методы, даже иногда графические.
Все это (и не только это) тривиально сводится к типам.
> Та же теорема Ферма, доказанная через эллиптические кривые - никому ведь ранее даже в голову не приходило связать одно с другим.
Эллиптические кривые - всего лишь тип в инфинити групоиде, изоморфных которому там полно. В том числе таких, использовать которые в доказательстве теоремы Ферма никогда не придет в голову вообще никому и никогда, потому что мозгов не хватит.
>Хцдевс
Эта та конфа для фронтендеров-шизиков?
Там вообще новости какие-то обсуждают, и говно бесполезное не учат.
Как прикрутить это все к c++?
Берёшь и без задней мысли прикручиваешь
По хаскелю и коммон лиспу должно быть больше гайдов, можешь погуглить сначала их
Даже к жабаскрипту прикручивают вовсю. Просто берется нужная логика (например, PTS) и пишется на интересующем яп.
Настоящие математики-профессионалы ссут на вашу теорию типов
Надеюсь в этих ваших пруверах
(sqrt(2) == 1.4142135623730951) == false
Иначе говно без задач.
(sqrt(2) == 1.4142135623730951) == false
Иначе говно без задач.
>1.4142135623730951
Главное чтобы прувер стек оверфлоу не словил, а так всё нормально.
Даже так можно codewars com /kata/5d2b89d4b90c0a001f4a6456
это неправда, так как я видел математиков профессионалов, которые занимаются физикой и создают модальную HoTT для своих нужд
> реально написать
This.
Дело в том, что √2 никак не может равняться 1.4142135623730951. В математически точных языках редуцируются только редексы(√2 не есть редекс). В математиматически точных языках выражения фактически равняются числам. Т.е √2 это число. Как и ⅓, к примеру.
Ни это
1414213562370951 / 1000000000000000
(1414213562370951 / 1000000000000000) = 2
Ни это
1414213562370951 1414213562370951 <> 2 1000000000000000 1000000000000000
/\
1000000000000000 <> 0.
Ванильный петушара не может.
А сделать его неванильным не могу я.
1414213562370951 / 1000000000000000 x
(1414213562370951 / 1000000000000000) = 2
1414213562370951 x 1414213562370951 <> 2 x 1000000000000000 x 1000000000000000
Multiplication fix.
Продалжаю писать в свой личный тред.
Доказал:
Lemma sqrt2: forall x y,
(0 < x)%nat -> (0 < y)%nat ->
INR x / INR y <> sqrt 2.
Довольно урчу.
Где доказательство?
>Эллиптические кривые - всего лишь тип в инфинити групоиде, изоморфных которому там полно
Типа смотришь такой на картину Рембранта: картина это просто краски и холст, краски можно выбрать любые и холст любой.
HoTT все дальше и дальше от математики, после того как помер единственный математик у его основ. Уже бизнес кабаны подхватили.
>freek
Да я понимаю, что это аутизм, но зачем так грубо.
Как я вкатился в НоТТ на 350к/месяц. Топ 20 вопросов на собеседовании по НоТТ. Скидка 50% на курс "НоТТ с нуля" .
школота с идрисом съебитесь нахуй
А что с идрисом не так?
мимо
слоение хопфа запиши на идрисе
sloenie_hopfa : Bool
Очень интересная аутистская ерунда! Какую самую сложную теорему вы формализовали? Или доказали? Я просто еще не до конца понял, что тут происходит.
тут в /pr передержка для второгодников, они выписали гомотопические пруверы и рядом Идрис написали. Непонятно что одни доказывают, но вот видно IEEE754, умножение и равенство. В принципе с помощью Идриса больше ничего и не докажешь.
Идрис не прувер, в нем можно доказать bottom, нет контроля рекурсии, нет гомотопий, нет ничего, он экстрактит Си программы которые линкуюутся с stdlib и которые текут. Идрис для шотландских бомжей из ПТУ Святого Андрея.
идрис говно и моча
Идрис2 теперь работает без установленного первого идриса! Собственно, для установке нужен chez scheme.
https://github.com/idris-lang/Idris2
https://github.com/idris-lang/Idris2
> Идрис для шотландских бомжей из ПТУ Святого Андрея.
Идрис - первый в мире ЯП общего назначения на основе зависимых типов. Верифицированный код это будущее программирования в принципе.
Зачем идрис компилируется в схему? llvm бэкенд планируется?
Но это было будущее 20 лет назад. Оно плавно стало прошлым, так и не пройдя стадию настоящего.
> llvm бэкенд планируется?
Можно в С скомпилировать, а из него clang'ом в LLVM.
> Но это было будущее 20 лет назад. Оно плавно стало прошлым, так и не пройдя стадию настоящего.
Манямир. 20 лет назад про зависимые типы знали полтора математика из coq комьюнити. На идрисе сейчас обкатывается то, что в яп будет нормой лет через 10 минимум.
>Можно в С скомпилировать, а из него clang'ом в LLVM.
idris -> scheme -> c -> llvm ir -> object code
Охуительно. Толку от верифицированного кода, который проходит через все эти фазы трансляции, обогащаясь низкоуровневыми багами и даже логическими ошибками?
> idris -> c -> llvm ir -> object code
Поправил.
> Охуительно. Толку от верифицированного кода, который проходит через все эти фазы трансляции, обогащаясь низкоуровневыми багами и даже логическими ошибками?
Тогда так:
idris -> c -> compcert -> object code. Я думал, тебе именно LLVM нужен, а если просто чтобы было, то пикрелейтед. Опять же, надо пынимать, что Идрис это во многом полигон для обкатки вещей, в программировании общего назначения принципиально новых. Там вон у самого Брэди ошибки при установке, сам себе issues открывает один за одним. Ты хочешь чтобы снихуя все сразу работало, так не бывает. Авиация началась с того что братья Райт на своем поделии три метра пролетели. Ну и там есть механизм запиливания собственных бэкендов.
[code]
test
[/code]
test
[/code]
Ну дык че там, доказатели? Как светлое будущее?
Доказали что его не будет.
Светлого? Или будущего?
А почему нет таких работ, когда какой-нибудь аутист в качестве хобби формализует в одной из этих систем сложное, знаменитое доказательство? Последней теоремы Ферма, например, или чего-то такого.
Делают же люди дома из спичек, яхты в бутылках, модели Звезды Смерти, годами. А это чем хуже? Еще элитнее же выходит, не для быдла - должно быть привлекательно.
Делают же люди дома из спичек, яхты в бутылках, модели Звезды Смерти, годами. А это чем хуже? Еще элитнее же выходит, не для быдла - должно быть привлекательно.
Из спичек ты хотя бы можешь подержать в руках, сфоткать и кому-нибудь показать, поставить на полку. А абстрактный выхлоп в консольке никому не интересен, поэтому даже если кто-то этим реально занимается, известно это будет почти никому.
Популярность все это действо в целом какую-то имеет. Уже лет 20, если не 30, существуют норм пруверы. Постоянно делаются новые тулзы.
Даже ИТТ видно, что формальные методы привлекательны для некоторой прослойки задротов.
А самих доказательств, если рассматривать сложные теоремы за пределами школьного курса - пересчитать по пальцам одной руки старого фрезеровщика. Никто не копается углубленно, получается. Так, поверхностно поиграют с системой, и бросают. Недаром ИТТ (или в прошлом треде, не помню) большая часть постов была про установку и настройку редактора, лол. Такое впечатление, что на этом все и заканчивается.
Просто это действительно сложно. Высшая математика-то доступна меньшинству людей, доказательство теоремы Ферма - так вообще единицам. А этот человек ещё и пруверами должен увлекаться на серьёзном уровне.
Если ты знаешь математику, то тебе такая хуйня неособо интересна. Если не знаешь, то доказывать будешь школьное говно.
А там правда нужно прям знать математику? Если доказательство уже расписано где-то словами, то мне кажется больше инженерная, механическая работа. Раскопать определения, записать их на формальном языке, заполнить пробелы в доказательствах, закодить какие-то стандартные приемы. Ну то есть знать на университетском уровне надо, конечно, но прям чтобы математиком быть - сомневаюсь.
> Раскопать определения
> заполнить пробелы в доказательствах
> закодить какие-то стандартные приемы
То есть прошариться до уровня математика в этих рамках. Хуй ты что заполнишь или закодишь стандартные приёмы, если не понимаешь, что и почему происходит.
>то доказывать будешь школьное говно.
А мне норм.
Кстати, чому пруверам на учат в школе?
>Наш язык для просветленных социалистов, а не потребителей
>Кстати, чому пруверам на учат в школе?
А кто учить то будет?
Чет хохотнул, представив как средний школьник (АУЕ быдлан с потухшими глазами и гниющими от крокодила руками, из математики с трудом освоивший только сложение на пальцах в 15 лет) пыхтит над доказательством теоремы Пифагора в коке.
>средний школьник (АУЕ быдлан с потухшими глазами и гниющими от крокодила руками, из математики с трудом освоивший только сложение на пальцах в 15 лет)
Я имел в виду не ебеня Казахстана, а нормальные ДС-школы, не обязательно 57, но что-то более-менее приличное.
>что-то более-менее приличное.
Ну так гниющие, а не сгнившие. Чо ебало скорчил?
Нахуй вы это говно учите?
Спрошу тут. А почему программирование не пошло по такому пути? Ну скажем, описываем на некоем языке регистры процессора. Также описываем действия - то есть по сути регистры до, действие, регистры после. (Не только регистры, но и флаги, память, не суть). Потом описываем что должна делать программа (например вывести число на экран). А компьютер уже сам подбирает алгоритм, исходя из того что мы хотим получить (возможно мы задаем хинты, что важнее память или производительность, хотя по идее и это он сам может шедулить). Сам подбирает нужные команды процессора. Какие подводные камни?
Чтобы потом доказать на прувере что ты пидор.
Да никаких, собственно.
То есть описывать не последовательность действий (императивное программирование), а результат (декларативное)?
На практике получается, что результат надо описывать слишком подробно, потому что его надо декомпозировать на подрезультаты, которые, по сути, являются подздадачами, и в конце получается точно такой же императивный код, но вывернутый наизнанку.
Можно сравнить с рецептом, как я писал здесь
У борщехлёбов другое мнение, но кого оно волнует.
>На практике получается, что результат надо описывать слишком подробно
Почему? Пусть компьютер сам оптимально разбивает на декомпозицию.
Тебя недостаточно обоссали в прошлый раз и ты пришёл за добавкой, мудило?
Ну как он это сделает? Это всего лишь машина, которая не может сама думать и не может магически влезть в голову программиста, чтоьы понять, чего он хочет. Единственный способ - обернуть простейшие команды в более сложные, их ещё в более сложные, и так далее до привычных процедур. Всё, что можно сделать - немного изменить семантику на самом верхнем уровне, но под капотом будет то же самое.
В тот раз внятных аргументов, кроме РЯЯ ВРЁТИ, я так и не услышал, уверен, что не услышу и сейчас. Поэтому уходи.
Шо тут непонятного то? Программист задекларирует, например, что есть команда копировать файл. Опишет что вот у нас диск до выполнения команды, а после выполнения команды диск должен содержать дополнительную копию указанного файла. Что тут мешает компьютеру самому определить, какие действия надо провести, чтобы получить желаемое изменение?
По сути, компилятор для всего. Ведь это то же самое, что делает компилятор, когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение, разве нет?
Не совсем понятно, как это должно выглядеть. Так что ли?
исходное_состояние = [файл, ⚹]
прочее = исходное_состояние - файл
новое_состояние = [файл, файл, прочее]
эвм.начать_думать(исходное_состояние, новое_состояние)
Чем-то напоминает пролог. Ты не на него намекаешь? Деталей я не знаю, но, вроде, выяснилось, что он оказался не всесильным и слишком сложным для чего-то реального.
> когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение
Это оптимизация, а не игра в угадайку. Изначально никаких оптимизаций не задумывалось, предполагалось, что как пишет программист, такие инструкции и будут. Оптимизации же появились не чтобы решать задачи за программиста, а чтобы прозрачно для него ускорить работу выполнения кода.
> регистры до, действие, регистры после.
Хуя тут авангард мысли. Так и до логики Хоара додумаетесь, а может быть даже и до separation logic. Между прочим, программирование в стиле "дать комплюхтеру задачу, а он пусть сам ебется с ее реализацией", это ровно то, чем занимается например Брэди сотоварищи в рамках type-driven development. Но там пока все очень далеко от идеала, уточнять постановку задачи по ходу дела должен таки человек. К этому же в идрисе столько всяких кодгенов, во втором идрисе, например, третьего дня кодген js запилили. Т.е ты делаешь на идрисе чего тебе надо, а потом компилишь всю хуйню в жс итд.
> додумаетесь
Не я, для меня единственное доказательство корректности - тестировщики ничего не нашли, а на проде ни разу не остановились бизнес-процессы.
Тестированием можно выявить наличие ошибок, но не доказать их отсутствие. Для всяких кабанчиковых приложений и так сойдёт, конечно же.
Причем тут тройки Хоара? Они нужны только для проверки, а не для создания алгоритмов.
То что он описал, мне больше напомнило proof-search подход по типу LambdaProlog, но там тоже не алгоритм строится, а доказательство выводится.
OpenAI делают прувер для metamath на нейроночках: https://groups.google.com/forum/#!msg/metamath/D09W2QVR-_I/g_rsqGj0AAAJ
> прувер для metamath
HoTT бы автоматизировали, а метамат этот кому нужен? Там и нейроночки не нужны, записать его в BNF форме и генетические алгоритмы прикрутить, которые к слову, превосходят deepRL в играх атари, грамматической эволюции там более чем достаточно.
Зделоли: https://arxiv.org/abs/2009.03393
AI во всём превзошёл анона?
Оно там только пытается доказать теоремы, которые уже были доказаны в метамат. Делает это лучше других доказателей, но результаты все еще не сказать чтобы впечатляют.
И че теперь математикам делать, когда их автоматизируют
Вкатываться в автоматизацию.
Автоматизация доказательств не имеет смысла.
В программировании, даже если код суперуёбищный до такой степени, что никто не понимает как он работает - он всё равно выполняет какую-то функцию, он полезен.
А в математике блекбокс прувер который отвечает да/нет как раз не имеет никакой пользы, потому что в математике важнее "каким образом", "что это значит" и "что это нам даёт", а на такие вопросы манясетки конечно же не ответят, пока что их удел - разгадывать капчу.
Что ещё за блекбокс прувер? Прувер, которому нужно верить, потому что он прувер?
На эти вопросы ты отвечаешь, когда придымываешь само утверждение. Это отдельная задача от доказательства.
Ну и найс гоалпост мувинг, конечно.
По сути, так работает каждый портируемый оптимизирующий компилятор.
> Автоматизация доказательств не имеет смысла.
Сказал зумер. Судя по написанному дальше, вообще не понимающий о чем пишет.
Потыкал палочкой шизика.
Анус себе потыкай. На шизиках мир стоит!
Так вот почему мне так тяжело. Уберите мир плес.
Нет, атлант, держи.
А пределы можно доказывать? Где лучше?
Как тут codewars com/collections/mathematical-analysis ? Нахуй тебе это нужно?
Чем блять это говно на пиках отличается друг от друга, мне кто-нибудь может объяснить?
>отличается
Теория описывает методологию интерпритации объектов в определенном фрейме
Магия рун является всего лишь одной из интерпритаций объекта руны
Ну и ты долбаёбушка на правильном пути если начинаешь что-то подозревать
Наставь на путь истинный.
Тебе не нужен этот путь
маскот АГДЫ - официальная курочка
кто теперь агдоводы?
кто теперь агдоводы?
Это серьезная проблема. У кока - петух, у агды курочка. Это же кризис индустрии!
классика ("моя голубка, мой голубочек"): https://www.youtube.com/watch?v=csgz5x8TYws
За такие видео надо пермачить.
пригорело, конструшок?
тоже не понимаю почему синтаксис нельзя сделать проще
Нет, это повод нести яйца!
зделой
Белуга не несет яйца. Переходите на Белугу.
Коки не топчут белуг - не интересно
(записывает в блокнотик)
на третий день обсервации госпитализированный пациент продолжает идентифицировать себя с домашней птицей французской породы.
от предложенных рыбных блюд отказался, обосновав это своими сексуальными проблемами.
рекомендации: продолжать наблюдение.
>на третий день
Я тут с первого треда подсераю, прояви уважение, ёба
я наблюдаю только три дня, так что прошу извинить
В городе Колпино группа встречает группу буддистов, которых герои берут с собой. В новгородском посёлке Чудово, путники вынуждают сделать остановку. Там они встречают охотника Одноглазого, который от радости приглашает всех к себе в гости. Математик решает остаться следить за составом. На следующий день возвращаются Александр с Владимиром Павловичем, от которых Математик узнаёт, что Одноглазый оказался каннибалом и убил всех буддистов. Команда продолжает путь.
(энциклопедия метро)
(энциклопедия метро)
> от которых Математик узнаёт
А доказать?
Мамой клянусь.
Чтобы принять, что верифицированное доказательство корректно, нужно быть уверенным в корректности верификатора. И так по всей цепочке до железа, которое работает на физических объектах, точность которых невозможно гарантировать. Приходится верить, что все работает как надо.
Какая тогда принципиальная разница между верифицированным автоматически доказательством и обычным, проверенным вручную?
Какая тогда принципиальная разница между верифицированным автоматически доказательством и обычным, проверенным вручную?
Машина ошибается гораздо реже чем человек, и чем сложнее задача, тем больше вероятность ошибка человека. Например попробуй перемножь две матрицы хотя бы 10 на 10 вручную, с огромной вероятностью ты допустишь много ошибок, в то же время компьютер их перемножит за долю секунды абсолютно правильно.
Зачем что-то проверять, если могут свет вырубить.
Выходит, это все опять же про вероятности. Так это не отличается от принятия доказательств голосованием, как это сейчас делается. Там тоже, чем больше седобородых мудрецов одобрит доказательство, тем оно вернее.
Се ля ви, абсолютной истины не существует.
>Чтобы принять, что верифицированное доказательство корректно, нужно быть уверенным в корректности верификатора
Как-бы нет, нужно не самого субъекта проверять, а сам объект.
Так Idris же вроде язык общего назначения, с элементами прувера.
Для освобождения человека от работы по проверке доказательств вручную
Что скажете про model checking, в частности, Spin?
никогда не думал, что напишу сюда
никогда не думал, что напишу сюда
Linear Dependent Type Theory for Quantum Programming Language
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"
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"
> Ну как он это сделает? Это всего лишь машина, которая не может сама думать и не может магически влезть в голову программиста, чтоьы понять, чего он хочет.
GPT-3
Естественные языки плохо формализуются, да и даже если попытаться, писать пришлось бы ещё больше, чем на языке программирования, ибо человеческие языки громоздки, нерегулярны и с произвольной трактовкой.
> GPT-3, сделай имиджборду на vue.js, пусть тема будет оранжевой, а маскотом будет Холо.
O'rly? Думаешь это короткое приложение больше чем исходный код, который сгенирирует GPT на выходе?
Это прям-таки всё? Не нужно описывать, что такое имиджборда и vue.js, какие решения принимать по умолчанию для не упомянутых параметров? А если нужно, чем это лучше процедуры generate_imageboard(framefork="vue.js", theme="orange", mascot="Holo") ?
> Не нужно описывать, что такое имиджборда и vue.js
Не нужно. Знания об этом уже есть в GPT-3.
> какие решения принимать по умолчанию для не упомянутых параметров?
На усмотрение GPT. Сделает максимально дефолтный вариант.
Звучит круто. Раньше натыкался только на проект, где по словесному описанию рисовалась картинка, работало, вроде, на нейронках.
Ты про DALL-E? Он также работает в связке с GPT-3. Сейчас возможности GPT-3 по программированию ограниченны, но это только потому что в датасет не были включены сорсы из гитхаба. Как только будет выкачен GPT-4 (надеюсь, с гитхабом), GPT-3 станет не просто мощнейшим инструментом программиста, он сможет заменить его end-to-end в большинстве задач, связанных с айти: написание сайтика, поиск багов, тайпчекинг, написание компиляторов, любых программ, на любом языке программирования. И кроме всего прочего, сделает тебе красивую md-документацию для сгенерированного кода.
Мы на пороге революции.
> DALL-E
Возможно. Не помню, давно читал тот пост где-то.
> Мы на пороге революции
Ждём.
Сверстанный текст на ЛаТеХе выдают за код (неведомого) прувера?
Ты не понимаешь, о чем пишешь. 1+1=2 безотносительно того, отключат свет или нет. То же самое с любыми правилами построения в прувере. А вот горький петух со своим форсом гпт3+ вполне может оказаться прав, итеративный файнтюнинг таких нейроночек + внешние средства проверки правильности типа того же прувера, могут реально толкнуть вперёд всю эту тему настолько, что свидетелям эйдосов и "превосходства человека над бездушной машиной" может реально поплохеть от возможностей автоматизированного доказательства. Не будем забывать, что по-сути, простой брутфорс обьебал в шахматы Каспарова ещё в 1997 году.
>горький петух со своим форсом ... таких нейроночек
съебите со своими нейтроночками, плиз, все доски уже засрали, чесслово. мы тут о высоком, а они всё о своём.
>Каспарова ещё в 1997
вы приводите Каспарова в качестве примера прувера? иначе зачем?
> мы тут о высоком,
А это и есть высокое, выше некуда.
> вы приводите Каспарова в качестве примера прувера? иначе зачем?
Куда тебе до высокого, если ты даже такой элементарный пример понять не в состоянии.
>А это и есть высокое
>Куда тебе до высокого
ваш "ИИ" пузырь раздули инвесторы всего несколько лет назад.
еще через пару лет инвесторы выйдут со своими деньгами (иначе зачем они заходили), а бывшие МЛ-стартаперы побегут за новым хайпом хвалить что-то новое "высокое".
анон гарантирует это
Да-да, немного потерпеть и прогресс остановится.
прогресс не остановить
40 лет назад пруверы работали кое-как и велись исследования
в наши дни пруверы работают кое-как и ведутся исследования
и еще через 40 лет пруверы будут работать кое-как и еще активнее будут вестись исследования
потому что пруверы - это о высоком
это компутер сайенс и рисёрч, а ваши вшивые стартапы
это прогресс
> 40 лет назад пруверы работали кое-как и велись исследования
40 лет назад пруверов не было, гейний. Automath не прувер.
>Automath
сами себе ответили
>А кто будет сторожить сторожа?
можно ли верифицировать Coq в Coq? или хотя бы в агде
> Кстати, чому пруверам на учат в школе?
А какое-то математическое ПО вообще используют в школе? Может в вузе?
В вузах разве что Matlab/Mathcad, но это всё не то.
>математическое ПО
Эксель
Бля, нам один препод в течение нескольких курсов давал один и тот же курсач, где надо было в ебучем экселе построить модель со сложной статистикой, и мы там юзали огромные формулы со всякими ДВССЫЛ и СЦЕПИТЬ, графики, сводные таблицы, фильтры, сортироввки, охуеть вообще.
разъясните за незаконность, плз
Не стоит вскрывать эту тему.txt
только самое веселое началось по телевизору, как сразу "детям пора спать".
где вы видели незаконный прувер?
это вам не статические анализаторы или инструменты фаззинга, тут все тихо и академично.
на Ada+Spark летают ракеты, но это никого не интересует, это и так все знают.
Написал hello world и калькулятор, — вот и молодец. На этом стоп. Не стоит вскрывать эти конпеляторы и гитхабы. Это тебе не колидоры вычистлительных центров НАСА, даже не датацентры ГУГОЛ, не уютненькие офисы ФЕЙСБУКА. В сферу IT лучше не лезть. Серьезно, любой из вас будет жалеть. Лучше закройте Хабрахабр и забудьте, что тут писалось. Это все вранье, чтобы привлечь как можно больше новых макак на рабочие места и создать демпинг зарплат. Я вполне понимаю, что данным сообщением вызову дополнительный интерес у воротил из Cisco, SAP и IBM, но хочу сразу предостеречь пытливых — стоп. Зарплаты у IT-шников очень унылые. Остальным их просто не дают.
>Это — борда для обсуждения ковариантных функторов, анафорических макросов, пандорических захватов, кластеров метапарадигм, катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов, ненужности математики, наконец.
>ненужности математики
Ахаха. А математике твои пруверы нахер не нужны.
И что теперь?
Даже тред в /pr запилили, а не в /math, наверное, потому что там уже есть загон для подобных шизиков в оснований-тредах.
Всё верно.
На сильную систему типов почему-то надо получать лицензию, на слабую нет.
кто выдает лицензию?
Государственная комиссия по радиочастотам?
на куртяник Agda|Coq уже есть лицензия?
вы же в курсе, что Thierry Coquand [Coq] & Catarina Coquand [Agda-1] не случайно имеют одну фамилию
где тот человек, который тут писал про собственный язык "говяжий"? у него что-то получилось? превзошел NuRPL и Twelf?
После получения базового теоретико-категорного mind-set от вебмакакинга тошнит, аж трясет, блядь. Интересно, что дальше будет.
В конце ты сдохнешь
Да ты просто в интерфейсах не разбирается, чтобы для них категории применить.
Требую scratch для пруверов!
Куда тебе в пруверы, если ты писать не умеешь
Парни, а о чем тред?
я даже это не осилил
я даже это не осилил
Вот есть типа книги по математики там. И там теоремы всякие. Они доказываются как на картинке и их никто не проверяет, просто люди от балды лепят себе звания академиков там всяких.
И пошла идея, что надо, чтобы компьютер доказывал так как он не особо может давить авторитетом. Пока что не очень получается так как давление авторитетом всё же происходит через непонятный синтаксис с кучами страшным значков.
А доказательство это типа про типизацию.
тред об том, как сделать, чтобы ракеты не падали мимо цели, и чтобы рентгеновский аппарат не просверлил поциента лучом внезано из-за опечатки васяна-прогламмера. впрочем, БОИНГУ даже это не помогло.
впрочем, не программистам верифицировать программы, этим должны заниматься профессиональные логики и математики.
имею ввиду верифицировать подобного рода софт, который относится к ракетостроению, например.
> даже это не помогло
Вывод: неработающая хуйня без задач.
/thread
Т.е автоматическая проверка софта на соответствие нормам и необходимым критериям?
Ну он понял, что роботы захватят мир и решил им не помогать. Забросил в 2к17 судя по гитхабу
Софт пишешь руками
Критерии пишешь руками
Пруфы, что софт соответствует критериям пишешь руками
Прувер проверят внезапнокорректность пруфа.
Верифицировать недоеденное дедовское говно типа С готовый софт - дело изначально не очень. Compcert и VST для кока и вот это все ящитаю путь в никуда. Нужно сразу писать корректный код, именно для этого делается Идрис, особенно Идрис 2. Сразу написал что тебе нужно и сконпелял нужным кодгеном в нужный формат. Брэди пока единственный шарит куда нужно воевать в плане средств написания корректного софта, остальное это полумеры и костыли. Алсо, он очень молодец что дропнул хачкелепомойку, теперь Идрис 2 ставится одной командой в бубунте с помощью стандартного snapcraft'а. Алсо, не стесняется признавать своих ошибок, так и сказал, что первый Идрис нормально не допилить, а QTT лучше чем его подход, на тему которого он написал диссертацию.
>QTT
>диссертацию
Хватит пугать.
Тред о том, что шизики-конструктивисты всё ещё пытаются сделать вид, что они могут в математику, и что они вообще нужны.
Их периодически пытаются пидорнуть из /math, вот они в /pr и перекатываются.
ЯМы хотим пруфать код. Гомологии и пучки тут никому не интересны
>ЯМы ...
... Алексей Навальный!
Свободу политзаключенным!
Россия будет счастливой!
разве это не замечательно, когда собравшиеся доны после более года куртуазных обсуждений где-то в районе 365-го сообщения начинают ВНЕЗАПНО выяснять, о чем же был, собственно, этот тред.
код пускай пруфает солвер (осталось его написать).
человек нужен только, чтобы задавать вопросы сочинять спецификации и архитектуру.
"компьютер бесполезен - он может только давать ответы" (с) Пикассо
>осталось его написать
Бля хуйня какая. Что же сразу не сказали, ща напишу.
Хлебаем борщи уже больше двух лет, а он только опомнился
У меня складывается впечатление, что кроме меня тут с верификацией кода вообще никто не сталкивался. А потом пришел модульный долбаеб без мозгов пучками трясти... Но я всё-таки спалю годноту быдлу, новый 5ый том software foundation https://softwarefoundations.cis.upenn.edu/ полностью посвящен основам этого дела на примере кока и уже упоминавшегося мной VST с написанным для него верифицированным подмножеством С. Я не перестал считать это направление путем в никуда, но как введение в предмет - вполне годно.
>А потом пришел модульный долбаеб без мозгов пучками трясти...
Что ты имеешь против математики?
> Что ты имеешь против математики?
Ничего. Модульный долбаеб != математика.
Ну тогда хорошо.
>с верификацией кода
И что ты такого делал?
верифицировал, что 1+1==2
Читать научись, маня. Там про код написано.
Формально верифицировал, что noop ничего не возвращает и то что функция identity возвращает свой аргумент.
>кроме меня тут с верификацией кода вообще никто не сталкивался
Наверное.
>на примере кока и уже упоминавшегося мной VST с написанным для него верифицированным подмножеством С
А что даст полная верификация всего С?
Любая программа на верифицированном С будет верифицированной?
Я не шарю.
>Я не перестал считать это направление путем в никуда, но как введение в предмет - вполне годно.
Почему это путь в никуда?
>Почему это путь в никуда?
>А что даст полная верификация всего С?
я не тот анон, но один ваш вопрос отвечает на другой.
Не выкайте мне, я с вами на вы не переходил, я не вы, а ты.
Спасибо.
Но я так и не понял, это путь в никуда, потому что полная верификация ничего не даст, или полная верификация - это путь в никуда?
Но ведь ты не я. А он отвечал мне.
Но ко мне тоже не надо на "Вы". Это же Двачи, тут принято хуями крыть, а не на "Вы" обращаться.
> Любая программа на верифицированном С будет верифицированной?
Да. Но его полностью верифицировать невозможно, хотя теми чуваками верифицирована бОльшая часть.
> Почему это путь в никуда?
Потому что С не про верификацию, его создавали без учёта таких возможностей, это уже недавно придумали. Как я говорил выше, правильный путь - изначально верифицированный код. И лучший вариант это написание кода на чем-то одном, а затем его компиляция кодгенами во что угодно, как и работает Идрис 2.
> Но я так и не понял, это путь в никуда, потому что полная верификация ничего не даст, или полная верификация - это путь в никуда?
Полная верификация С невозможна, что доказал Аппель сотоварищи. А та часть, которая таки верифицируема, ее намного проще генерировать кодгеном в идрисе.
> > Любая программа на верифицированном С будет верифицированной?
> Да.
Для того, чтобы программа на С была верифицирована, ей же нужна спецификация, не? Т.е. любую программу на С надо или переписывать, или дописывать. Без спек, можно доказать отсутствие UB, "корректность" работы с памятью и проч.
Что я не так понимаю?
мимо пятую книгу не читал
Вот представьте себе - верифицировали тот же Идрис на Идрисе, к примеру. Никаких сомнений уже нету. А потом вдруг выясняется, что система типов такая, что можно доказать Bottom. BINGO! Потом ее пофиксили, а через год опять нашли новый Bottom. А через год опять. Bottom - это полная жопа, никто не застрахован.
Замечательно же. Язык на котором, чтобы обосраться нужно постараться, лучше чем наоборот.
Бамп.
>Bottom
Что это?
Возможно ли теоретически построение верификатора, верифицирующего самого себя?
Или это алгоритмически неразрешимая задача?
Теорема Геделя в помощь.
> Теорема Геделя в помощь.
Педеля. Не знаешь - не неси хуйни. 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="Ваш+жалкий+практический+земной+мирок+не+нужен"
Человек-мем.
и ни слова о контрактном программировании, что характерно
Интересный тред. Жаль я не программист.
Доказательства это гиблое и не нужное дело, нужно развивать систему тестирования. Тот же Эвклид уже не нужен так как есть аналитическая геометрия, где ничего доказывать не нужно, а просто и понятно работают над векторами.
Нормальный учебник по аналитической геометрии начинается с аксиоматики. Но откуда тебе это знать, в твоем заборостроительном вузе.
Обычно как раз в конце в силу традиции дедов.
Свободный инструментарий для доказательства теорем Coq рассматривает возможность смены названия. Причина: для англофонов слова "coq" и "cock" (сленговое название мужского полового органа) звучат похоже, и некоторые пользователи-женщины, сталкивались с двусмысленными шутками при использовании названия в устной речи. Само же название языка Coq произошло от фамилии одного из разработчиков, Thierry Coquand. Сходство звучания Coq (фран. петух) и Cock (англ. петух) уже обыгрывалось в проекте: язык, используемый для описания конструкций, называется Gallina (лат. курица).
> Coquand.
Кукан епт
Какая разница, как называть, главное чтобы работало. А название пусть хоть крокодилзалупасыр будет.
>пользователи-женщины,
А coqомрази могут и потерпеть
Какая разница как назвать нигеров, главное чтобы работали))0
идрис говно и моча
Да, но почему ты это написал?
Первая или вторая версия?
вторая хуже первой
могу себе позволить
Какого хуя?
Во второй 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 :))
Идрис это больше про корректный код, а не про прувер. Современный код настолько примитивен, что даже парадокс Жирара в системе типов не мешает. Алсо допилят же, там до первого релиза ещё как до Луны пешком. Огромный плюс в идрисе2 уже в том, что дропнули хачкелепарашу, в итоге все ставится одной командой, работает быстрее и не тянет гигабайты говен. Алсо, второй Идрис совместим с плагином для первого в атоме. Там вот ещё что запилили:
> 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.
Автозаполнение дыр теперь работает на уровне всего кода.
> 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.
Автозаполнение дыр теперь работает на уровне всего кода.
Добавлю.
> 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, завезут в мейнстрим.
> 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 лет уже. Если кому-то надо разрешимый вывод для любой системы типов, с нынешними вычислительными мощностями это очень условная проблема.
> Курица или Петух, никогда даже близко не догонят.
Они и не для этого вообще-то. Даже Идрис это больше испытательный полигон для методов, которые завезут в мейнстрим.
> >Прувер
> О чем тред?
Поддвачну вопрос.
Об автоматическом доказательстве теорем. Записываешь теорему с определениями на неком формальном языке, понятном пруверу, а он говорит, долбоёб ты или нет. Правда, ни один анон в этом треде дальше школьного говна по алгебре не продвинулся. Интереса к хуйне без задач мало, почти за два года бамплимит не был достигнут.
Я видел MS сильно дрочит на доказательства https://project-everest.github.io/ , ещё видел ats. Это же рилейтед, т.к. идрис и lean4 в шапке. spark же взлетел.
Большинство пруверов не умеют ничего доказывать автоматически. Доказательство ты пишешь ручками, а он лишь проверяет, правильное ли доказательство.
Причем тут Property-based testing? Разрешимость даёт мне то, что я просто пишу код, а конпелятор сам его проверяет. Неразрещимость означает, что я должен какие-то типы сам в голове вычислить и конпеляту указать, чтобы программа прошла тайпчекер. Причем тут вычислительные мощности? Неразрешимость означает что у уравнения в принципе нет решения, какие бы вычислительные мощности там ни были. Нужно руками всё делать, без комплюктера.
Ты не понимаешь смысла неразрешимости вывода типов в какой-то теории типов. Не надо это путать с неразрешимой в принципе задачей.
> . Неразрещимость означает, что я должен какие-то типы сам в голове вычислить и конпеляту указать, чтобы программа прошла тайпчекер.
Вера швятая во магическую "вычислимость в голове", чем-то отличающуюся от вычислимости в общечеловеческом смысле.
блять, чувак, можешь вот таким же понятным языком с минимумом групоидообразных выебонов рассказать, что сейчас есть авангард мысли, в чем актуальные проблемы?
Он не может. Во-первых, этот анон имеет очень хуевое представление о чем он пишет, потому что он нахвался хуев по верхам в понве и смежных с ним раковниках. Во-вторых, это крайне абстрактная хуета и бытовым языком не излагается. Но это ничего, потому что применимость у нее околонулевая, и если бы не попил грантов - была бы нулевая.
Раньше ведь никто не писал теоремы в таком виде типа пусть там... Что вообще за поехавший придумал начинать что-то со слова пусть?
>Что вообще за поехавший придумал начинать что-то со слова пусть?
Секретов математики перечитал... Зочем это в нашем кружке аутистов?
> он нахвался хуев по верхам в понве и смежных с ним раковниках
Я даже не знаю, что это такое.
> Но это ничего, потому что применимость у нее околонулевая, и если бы не попил грантов - была бы нулевая.
Ну раз так сказал зумер с лгбт-пельменницей симплдимплом / попитом наперевес, наверное так оно и есть...
>что сейчас есть авангард мысли
ТНН
Поясните на какой-то теореме какое отношение она имеет к типам данных
Объект типа стал доказательством... что за птичий язык-то и что за пустой тип
Поридж, хоспаде... Теорема записывается в виде типизации. Если теорема верна, она соответствует непустому типу, если неверна - пустому. Ну и ещё есть вариант с потенциально бесконечными типами.
>в виде типизации
Значение знаешь?
Тралить пришел? Давай досвидули, /б вон там ->
Так это работает для полторы теорем, что конструктивные?
->
->
Как только конкретные вопросы о применимости изоморфизма, то маняматики сливаются.
Axiom of choice впиливается в одну строчку в 95 % пруверов.
Ok
Есть ли тут еще lean-дрочеры? Ну и как оно вам? Когда MS запилило 4 версию сломав обратную совместимость, а комьюнити форкнуло 3 и теперь пилит ее. Жопу рвет или норм?
Надо было 3to4 написать
>Жопу рвет или норм?
норм
Почему?
Какая разница во что поиграцца - денег этим всё равно тут никто не зарабатывает
Почему бы тогда не играться с петухом?
Не знаю. Мне понравилось
А почему должно рвать?
Там всё равно старый синтаксис впиливается штатными средствами.
Чем lean лучше петуха?
Если брать 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)
- Все термы в coic имеют вычислительный смысл, это не религия в которую надобно веровать
- Какой тогда вычислительный смысл у конструктора (индуктивного типа)?
- Он тривиальный
(из бесед с конструктивным петухом)
- Лямбада исчисление абсолютно, идеально, на нем будут писать инопланетяне, можно сказать что это Язык Бога
- А что вы скажете по поводу других вычислительных формализмов?
- Ну они тоже в принципе ничего
(из интервью Вадлера)
- В теории типов все правила интродакшена и илиминейшона идеально сбалансированы, это имеет глубокий вычислительный смысл
- Вот true терм, вот его интродакшен, илиминейшона нет - потому что не нужно
(с лекции Харпера про HoTT)
Что за пидорский такой термин "subject reduction"? Вроде пишут что это тоже что type preservation, так почему бы так и не писать - так ведь сразу понятно о чем речь мне.
А Lean неполноценный прувер? Ты шизик?
>верифицированного софта есть Идрис2
Верифицированный софт можно при желании хуярить на всём вышеперечисленном.
система типов вредна для верификации софта
Система типов полезна при доказательстве теорем.
>при доказательстве теорем.
Но за это деньги не платят
>деньги не платят
Съеби с треда. Заебали
Кому как.
1
Апну темку.
Скажите, имеет ли смысл вкатываться в эти ваши пруверы для лучшего понимания математики?
Если я, например, не пониманию логику доказательства теоремы, могу ли я переписать ее в код и посмотреть как это пошагово происходит? Покажет ли мне софтина промежуточные этапы?
Скажите, имеет ли смысл вкатываться в эти ваши пруверы для лучшего понимания математики?
Если я, например, не пониманию логику доказательства теоремы, могу ли я переписать ее в код и посмотреть как это пошагово происходит? Покажет ли мне софтина промежуточные этапы?
нет. мат. логика это параша, интересная лишь малой части математиков, и еще более малой части прогеров, желающих илитарности
В настоящей математике рассуждения более высокоуровневые как и в программировании.
>В настоящей математике
>В настоящей
Ловите илитария, лол
Правильный путь воина примерно таков:
почитать про metamath
разобраться с доказательством 2+2=4
написать интерпретатор mm
создать систему под себя с нужными тебе аксиомами и правилами вывода
доказывать то что тебе интересно в ней
(опционально можно metamath на hol заменить)
С другой стороны если ты не можешь создать такую систему которая механически
подтверждает твои выкладки можно ли вообще говорить о наличии понимания того
что ты делаешь?
>Покажет ли мне софтина промежуточные этапы?
Покажет, только они будут настолько тривиальными и их будет настолько много, что ты не сможешь ничего прочитать. По тем же причинам, по которым не можешь понимать программы в байткоде.
Что-то ты много хочешь. Иди нахуй
Спасибо за инфу, аноны.
В общем, насколько я понял, это всё не совсем то, что мне нужно.
Все эти метаматематики объясняют сложное с помощью еще более сложных и упоротых слоев абстракции.
Мне же нужно нечто совсем другое.
Чтобы было возможно посмотреть на обычное доказательство, но так сказать интерактивно, в процессе. Есть ли вообще такое?
Ну вот че не сделать прувер с таким синтаксисом как в скале
Дебил в треде. Зачем нужны зависимые типы, когда есть тройки Хоара? Я бы вообще выкинул из языков все типы, как в Питоне, и оставил бы только тройки Хоара. Почему так не сделают?
сурс
Потому что те кто пилят пруверы не полные ебланы в основном
> anonymous function
Это же лямбды, они везде примерно такого синтаксиса. Разница между тем, что на твоём пике, и скажем тем что в коке или агде в том, что в последних типизированная лямбда, т.е для всех термов нужно указать ещё и тип. Всё, остальное ровно так же. Типизированная лямбда даёт гораздо больше возможностей.
> Зачем нужны зависимые типы, когда есть тройки Хоара? Я бы вообще выкинул из языков все типы, как в Питоне, и оставил бы только тройки Хоара. Почему так не сделают?
Затем, что при сколько-нибудь сложном выражении тройка Хоара {P} c {Q} требует полного пересчитывания всех термов, а это не только >99% бесполезного труда, но и не всегда возможно. Есть более продвинутый вариант троек Хоара - separation logic, где считаются только непосредственные изменения, но и они нахуй не нужны, ибо сводятся всего лишь к зависимому сигма-типу. То есть, твое предложение сводится к тому, чтобы заменить все зависимые типы на один сигма-тип. Сделать это можно, но в итоге это приведет к выбрасыванию на помойку 90% возможностей зависимых типов.
> Все эти метаматематики объясняют сложное с помощью еще более сложных и упоротых слоев абстракции.
> Мне же нужно нечто совсем другое.
> Чтобы было возможно посмотреть на обычное доказательство, но так сказать интерактивно, в процессе. Есть ли вообще такое?
Тактики в коке разве что. Там весь процесс доказательства можно вывести пошагово.
> Затем, что при сколько-нибудь сложном выражении тройка Хоара {P} c {Q} требует полного пересчитывания всех термов
В компайл-тайме?
Объясните плез
Есть 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
Есть 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
получилось так:
length (trunc xs ys p q i j) =
isSetℕ (length xs) (length ys) (cong length p) (cong length q) i j
тред вмер
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