Программирование


Ответить в тред Ответить в тред

<<
Назад | Вниз | Каталог | Обновить тред | Автообновление
265 24 101

Пруверов тред #4 Аноним # OP 04/11/19 Пнд 08:52:13 15126741
Arend background.png (126Кб, 1305x506)
1305x506
Hottbookcover.png (42Кб, 300x432)
300x432
Anders Mörtberg.jpg (74Кб, 958x960)
958x960
Zorn’s lemma.png (57Кб, 531x250)
531x250
Тред успешных хлебателей борщей (очередной).

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
Аноним 04/11/19 Пнд 10:20:37 15127152
Аноним 04/11/19 Пнд 10:25:42 15127173
На этом вашем Петухе хотя бы интернет-магаз то реально написать, или очередной высер без задач?
Аноним 04/11/19 Пнд 10:26:59 15127194
>>1512717
>интернет-магаз
Наш язык для просветленных социалистов, а не потребителей
Аноним 04/11/19 Пнд 10:40:31 15127235
>>1512717
Сынок, ты не понял. Это — борда для обсуждения ковариантных функторов, анафорических макросов, пандорических захватов, кластеров метапарадигм, катаморфизмов, эпиморфизмов, анаморфизмов, параморфизмов, ненужности математики, наконец. Никого здесь твои слесарские проблемы не волнуют. Ваш жалкий практический земной мирок не нужен. Съеби.
Аноним 04/11/19 Пнд 10:50:48 15127286
>>1512723
Что за псевдонаучные термины? Что-то из вашего очередного брейнфака?

>>1512719
>социалистов
*Борщехлебов
Поправил тебя
Аноним 04/11/19 Пнд 10:52:40 15127307
>>1512719
А я говорил что ФП это марксизм
Аноним 04/11/19 Пнд 11:03:14 15127378
ОП, ты таблетки принял?
Зачем ты такие треды создаешь в белом интернете, это незаконно вообще то.
Аноним 04/11/19 Пнд 11:19:41 15127449
>>1512737
Да в /pr все вне закона, кроме вкатывальщиков.
Аноним 04/11/19 Пнд 14:05:32 151285710
>>1512674 (OP)
И зачем? Тут никто ничего нового и не прочитал ещё. Приходи через пару лет.
Аноним 04/11/19 Пнд 14:20:44 151287611
>>1512717
СОQ тьюринг полный, можно написать всё что угодно.
Можно написать интернет магаз из которого гарантированно нельзя украсть деньги. Только писать нужно всё самому, начиная от сетевого стека и базы данных.

Если очень хочется, можно посмотреть на `coq.io`
Аноним 04/11/19 Пнд 14:23:08 151287812
>>1512876
Как доказать что функция тотальна, если кок не понимает, что я уменьшаю аргумент?
Ты выглядишь шарящим.
мимо
Аноним 04/11/19 Пнд 15:05:59 151293713
Очередной тред для пиара Максимки Сохацкого?
Аноним 04/11/19 Пнд 15:20:43 151296014
>>1512937
Да хоть в тапки ему нассать. Лучше пруфать научите.
Аноним 04/11/19 Пнд 15:26:51 151296515
Аноним 04/11/19 Пнд 15:47:33 151298416
>>1512878
На натуральных числах должен просто работать паттерн-матчинг.
Для остальных - хз.
Аноним 04/11/19 Пнд 15:55:44 151299517
>>1512984
Ну это только для снятия S работает. А вдруг я поделить и/или вычесть хочу. Он уже не понимает. Как подсказать то...
PS можно дополнительный аргумент протаскивать, но потом надо пруфать, что он на результат не влияет, а мне тяжело.
Аноним # OP 05/11/19 Втр 06:47:44 151353018
Аноним # OP 05/11/19 Втр 06:53:35 151353419
>>1512878
В 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».)
Аноним 05/11/19 Втр 11:28:26 151361920
Хватит заниматься этим фуфлом!
Аноним 05/11/19 Втр 18:18:20 151392921
>>1513619
Это по любви. За остальное надо требовать деньги.
Аноним 06/11/19 Срд 20:27:16 151490322
15728009281210.jpg (345Кб, 1920x1296)
1920x1296
Зумера вкатывальщики не могут в пруверы по причине отсутствия мозгов. Но даже если зумер осилит кок, это не даст ему ничего, потому что он все равно не может в математику, т.е даже в элементарное практическое применение того же кока.
Аноним 07/11/19 Чтв 04:17:24 151512723
Оп, почему нет этого прувера https://arend-lang.github.io/ вроде интересная тема. Как минимум потому что там HoTT это основной язык, а не костыли над основным, как в коке или агде, ставится в полтора клика как плагин к IntelliJ, есть обзор на швабре https://m.habr.com/ru/company/JetBrains-education/blog/469569/
Аноним 07/11/19 Чтв 04:50:31 151513224
>>1514903
Да не гори, осилишь ты кок.
Аноним 07/11/19 Чтв 04:59:35 151513525
Аноним 07/11/19 Чтв 06:51:22 151515126
>>1514903
Почему так мерзко от пика?
Аноним # OP 07/11/19 Чтв 08:54:57 151517727
>>1515127
>почему нет
Предпоследняя ссылка в топике вообще‐то.

>а не костыли над основным, как в коке или агде
>агде
«agda --cubical» погугли.
Аноним 07/11/19 Чтв 10:06:25 151520328
>>1515177
> «agda --cubical» погугли.
Я это даже ставил. Отдельная либа же. Или что-то другое есть?
> Предпоследняя ссылка в топике вообще‐то.
Лол, в глаза долблюсь.
Аноним 07/11/19 Чтв 11:38:15 151525229
>>1515203
>Отдельная либа же.
Ну так там в ядро агдочки встроены кубические примитивы.
Аноним 07/11/19 Чтв 15:25:12 151542830
>>1515252
А ты случайно не в курсе, как Идрис поставить через stack, если его нет в stackage?
Аноним 07/11/19 Чтв 15:52:19 151547231
>>1515428
Не, я не пользуюсь ни шидрисом, ни stack’ом.
Аноним 07/11/19 Чтв 16:04:28 151549332
>>1515472
Как ты живёшь вообще?
Аноним 07/11/19 Чтв 20:06:47 151573733
Аноним 07/11/19 Чтв 22:44:58 151589734
А что с прошлым тредом? Неужели утонул? Какая жалость, кек.

Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
Аноним 07/11/19 Чтв 23:34:59 151594035
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



Аноним 07/11/19 Чтв 23:35:28 151594136
>>1515897
>аксиомы coic

Вот же дебил.
Аноним 07/11/19 Чтв 23:37:29 151594337
>>1515941
Первый верун порвался.
Аноним 07/11/19 Чтв 23:41:30 151594438
>>1515940
Что за система? Дерево вывода покажи с аксиомами.
Аноним 08/11/19 Птн 00:13:08 151595439
>>1512674 (OP)
>Arend background.png
\У \куска \говяхи \синтаксис \лучше
Аноним 08/11/19 Птн 00:14:42 151595540
>>1515944
>Что за система?
Обычное MLTT, лол
> Дерево вывода покажи
А в чём разница? Всё понятно же, а в латех лезть мне лень.
Аноним 08/11/19 Птн 00:16:00 151595841
>>1515940
Проебался, там вместо tr должно быть coe, но вы поняли.
Аноним 08/11/19 Птн 00:18:49 151596042
>>1515958
Нет непоняли нихуя, ты шизик что ли реально что за tr coe ap ★ наконец?
Аноним 08/11/19 Птн 05:56:31 151602643
15729840971980.png (61Кб, 500x441)
500x441
>>1515897
> Ну что пидараски, хоть 0 ≠ 1 знаете как доказать? А аксиомы coic разузнали, или все продолжаете веровать что швятой дух машины говорит швятую истину потому что так должно?
То, что у тебя нет мозгов, потому что ты зумер, не значит, что их нет ни у кого.
Аноним 08/11/19 Птн 07:35:32 151603544
>>1515954
Да нормальный синтаксис, быстро привыкаешь.
Аноним 08/11/19 Птн 09:11:23 151607045
Проблема унивалентных оснований даже не в том, что эту тему по-сути 3.5 тела тащат типа Мортберга, ещё и Воеводский помер, пиздец. Главное - конструктивная математика изначально малопригодна для прямого использования людишками из-за сложности построений. Ещё Брауэр писал, что его интуиционизм без проблем можно использовать только при наличии бесконечной памяти, т.к манипуляции со сколько-нибудь сложными ментальными построениями требуют гораздо больше мозгов, чем их есть у кого угодно. В наше время половина этой задачи решена - кудахтеры + HoTT, в общем дают возможность доказать что угодно, любая математика представима в унивалентных основаниях. Однако, все это не отменяет того, что большую часть пруфов надо писать вручную. А в случае сложной матчасти и на это тоже мозгов не хватает ни у кого. Даже Мочидзука свою IUTeich в унивалентных основаниях переписать не осилит. Нужна автоматизация подобного рода пруфов, причем, одними тактиками это сделать не получится. Идеи есть, как это реализовать, но времени нет совсем. То одна хуйня, то другая...
08/11/19 Птн 21:05:29 151652546
>>1516026
Серануть любой может, вот только доказательства все нет.
Аноним 08/11/19 Птн 21:11:42 151653547
Аноним 08/11/19 Птн 22:06:01 151656648
>>1516535
Ой дибил... дерево вывода где? Где аксиомы? Ты просто веруешь.

алсо
>>1516026
>То, что у тебя нет мозгов, потому что ты зумер
у убогих мандавошек проекции просто одна охуительнее другой.

>>1516070
>Проблема унивалентных оснований даже не в том
>можно использовать только при наличии бесконечной памяти
Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время". Хотя думаю нет - они ж были совсем не тупые как местная пидорва.
Аноним 08/11/19 Птн 22:09:53 151656749
Вы даже хуже Rust-борщехлебов.
Аноним 08/11/19 Птн 22:18:29 151657850
>>1516566
ты что дибил, дед? какие аксиомы? это ж чистое лямбда исчисление. тут только определение функции, аппликация, бета редукция и эта экспансия. Этого хватит чтобы доказать эту теорему.
Аноним 08/11/19 Птн 22:22:54 151658151
>>1516578
>ты что дибил, дед? какие аксиомы? это ж чистое лямбда исчисление.

Совсем дурак шоле?

>тут только определение функции, аппликация, бета редукция и эта экспансия. Этого хватит чтобы доказать эту теорему.

Тут как минимум нужен ещё J для равенства пути
Аноним 08/11/19 Птн 22:26:24 151658352
>>1516581
Нужно и равенство да, но если есть индуктивные типы для чистого исчисления (Cedile), то можно элиминаторы равенства и его бета (J) и эта правила (которое в не HoTT системах запрещено) написать в чистых функциях. Так то дед! Ты не совсем дибил если знаешь про J, но явно отстаешь от индустрии лет на 5.
Аноним 08/11/19 Птн 22:29:19 151658453
>>1516583
Плюс в кубиках J дерайвабл, так что J уже давно ни у кого не аксиомах (как минимум в PTS CiC системах типа Formality и кубиках).
Аноним 08/11/19 Птн 22:48:06 151659054
>>1516583
Ну вот мы и видим как еще один верун дристанул под себя. Естественно никакого дерева вывода можно не ждать, ведь ты не имеешь ни малейшего понятия как работает твоя система, а просто в нее веруешь.

>для чистого исчисления (Cedile)
>дает доказательство в lean
Максимальная маневренность. Хотя до чудика выше что дал доказательство в собственном маня-mltt еще далеко.
Аноним 08/11/19 Птн 22:51:21 151659255
>>1516590
Ты просто ни разу NbE не написал и живешь в бумажных деревьях, математик которые не может в дебагере выставить printf будем вопить и плеваться на анонимных досках, потому что в то время пока он будет рисовать никому не нужную макулатуру на бумаге, программисты будут писать за него теоремы о неподвижной точке.
Аноним 08/11/19 Птн 22:52:12 151659356
>>1516592
труси костями и ползи на кладбище со своими бумажками.
Аноним 08/11/19 Птн 22:54:45 151659957
>>1516593
ты вообще никому нахуй не нужен, можешь только в подворотням недостудентам про матанализ рассказывать с голоду. Ты даже в автоматизации математики бесполезен!
Аноним 08/11/19 Птн 22:55:18 151660058
>>1516599
Генценовские деревья выводов блядь он просит в третьем тысячилетии. Лол
Аноним 08/11/19 Птн 22:56:43 151660259
Аноним 08/11/19 Птн 22:57:38 151660460
>>1516600
Ну давай показывай тогда как ты доказываешь зумерок
Аноним 08/11/19 Птн 22:59:14 151660561
>>1516604
Я почитал все твои высеры на дваче, мистер Арнольд, перед свиньями бисер не бросаем, и вам не советуем. HoTT это секта не для челяди и совковых бумажных математиков.
Аноним 08/11/19 Птн 23:00:11 151660662
>>1516605
Сри дальше, а я буду смотреть через сколько лет ты разовьешься хоть во что-то или так и будешь передавать знамя невежества своим сынам и воинам долбоебизма.
Аноним 08/11/19 Птн 23:08:01 151661263
Подводим промежуточный итог:
Вопрос: докажите 0 ≠ 1.
Пруверо-пидорва: ссытся под себя и пускает слюни от собственной беспомощности.
Ясно.
Аноним 08/11/19 Птн 23:12:30 151661464
>>1516612
У тебя ж два доказательства на руках, на Agda и на Lean. Или у тебя проблема какая-то в коммуникации и ты не можешь прочитать книжку и вместо своего СДВГ ты лезешь в интернет и орешь "это не доказательства!", "Арнольд говорил компьютеры не нужны!". К чему это все? Мы можем тебе написать доказательство 0!=1 на всех MLTT языках не вопрос. Но во-первых ты не принимаешь эти доказательства. Я слабо верю в то, что ты не веришь что существует изоморфизм между генценовскими палочками и трейсом работающей программы на компьютере. Ты либо просто ебанутый либо человек с нарушенными коммуникативными способностями.
Аноним 09/11/19 Суб 00:13:38 151666565
>>1516614
>У тебя ж два доказательства на руках, на Agda и на Lean.
На агде можно вроде бы проще написать в одну строчку, за Lean-поебень не скажу. В коке я могу вообще одной командой это сделать - inversion - и готово, охуеть да как ловко? Только я спрашиваю на каких фундаментальных принципах основываются эти доказательства. Проблемы не с моими
>коммуникативными способностями
а только с мыслительными способностями местной пидорвы. Они даже не понимают о чем их спрашивают. "Ну раз система говорит что это так значит это так" - верунчики, что с них взять. Особо продвинутые еще могут про швятой изоморфизм спиздануть не к месту.
>ты не можешь прочитать книжку
>своего СДВГ
>Арнольд говорил компьютеры не нужны!
новые потешные проекции подоспели.
Аноним 09/11/19 Суб 01:08:46 151670266
>>1516665
Ты ж великий бумажный математик, построй категориальную модель инфинити топоса, заэкстракть оттуда язык внутренней логики и получишь вычислительную модель ТС.
Аноним 09/11/19 Суб 01:21:10 151671067
>>1516665
То он Арнольд, то воинствующий Кок-петушок уже.
Аноним 09/11/19 Суб 01:26:19 151671368
>>1516710
Коком из математиков уже никто не пользуется, кстати, он годится и используется сейчас только для системного программирования и верификации. Даже конференций по Коку нет масштабных, а все авторы Кока ездят на Lean конференции и пишут на Lean.
Аноним 09/11/19 Суб 02:03:33 151672269
>>1516702
А вот возьму и построю. Ты то что будешь делать, манька, так и будешь продолжать веровать и молиться швятому автоматону?
>>1516710
>То он Арнольд, то воинствующий Кок-петушок уже.
Манька запуталась в собственных маня-проекциях, так мило.
>>1516713
И что они там делают, рассказывают MS-блядям что уже есть система для нормальных людей? Накидай линков что ли.
Аноним 09/11/19 Суб 02:11:44 151672670
>>1516722
Это чисто математические тусовки, там даже математиков с ноутами на винде нет. Это спонсируется грантами евросоюза. Ну если ты можешь построить Модельнеые категории для инфинити топоса на слабых расслоениях симплициальных множеств, то уже будешь 6-й в списке тех, кто это сделал.
Аноним 09/11/19 Суб 02:14:22 151672771
EHrum-NWsAEP4mA.png (110Кб, 839x510)
839x510
>>1516726
Даже не 6-й, а 8-й уже.
Аноним 09/11/19 Суб 02:26:11 151672972
>>1516727
Интересно как ты собрался строить это? На бумажке стрелочки рисовать будешь или пьесу в трех ролях разыграешь?
Аноним 09/11/19 Суб 02:26:58 151673073
>>1516729
У Воеводского вон не получилось, у филдсовского лауреата то, я хочу посмотреть что ты высрешь!
Аноним 09/11/19 Суб 03:45:56 151673974
>>1516566
> Что то тут вспомнился "A term of length 4,523,659,424,929". Может Бурбаки так же думали что для их нотации просто "еще не пришло время".
Для их нотации время давно прошло. Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
Аноним 09/11/19 Суб 04:44:18 151674475
>>1516739
Он же математик, это называется синтетическая теория, как аксиоматика Гильберта или Вейля. А так то клован, да :-) HoTT же тоже синтетическая теория. Давайте запутаем его!
Аноним 09/11/19 Суб 06:39:06 151674876
>>1516566
>где аксиомы?
Аксиомы Lean?
https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

>дерево вывода где?
Вон тебе бумажка, сам выписывай. Я ебал такой хуйнёй заниматься.

>Ты просто веруешь.
Верую во что?
В то, что авторы Lean действительно написали то, о чём рассказывает та бумажка? Да, верую, не разбираться же мне в тоннах крестокода.
В то, что существуют контексты и переменные? Да, верую, что тут такого?
В propext? Да, верую, но в чём проблема?
В choice? Если надо, тоже уверую.
До чего ты доебался, петух?
Аноним 09/11/19 Суб 07:31:55 151675277
>>1516748
> Lean
Чем он вообще хорош? Когда-то это был первый прувер на основе HoTT, потом это выпилили.
Аноним 09/11/19 Суб 09:03:00 151676878
>>1515151
Потому что ты видишь потреблядей, оболочек, а не духовноразвитых людейчтобы это не значило.
Аноним 09/11/19 Суб 09:11:11 151676979
Нахуй это все нужно?
Аноним 09/11/19 Суб 09:13:59 151677080
>>1516769
Если такие вопросы задаешь, значит тебе это точно не нужно.
Аноним 09/11/19 Суб 09:16:54 151677281
>>1516770
Я и не собирался, просто хочу узнать зачем это вам.
Аноним 09/11/19 Суб 09:33:09 151677382
>>1516752
Из особых фич: метапрограммирование разве что. Ну квошенты, хотя этим никого не удивишь.
Ещё IO сразу есть, а не как в коке.
Четвёртая версия в кресты компилируется (ещё обещают, что она будет ниибаца быстрая).
Аноним 09/11/19 Суб 13:59:35 151685083
>>1516739
>Формализм для оснований не подходит, это и до Брауэра понимали. Алсо, ты всё-таки осилит разницу между аксиомой и правилами вывода с посылками, раз уж что-то кукарекаешь за конструктивную математику, а то выглядишь клованом.
О, неужели конструктивный петушок показал свой клювик с подпевалами? Давай расскажи мне как конструктивная математика не нуждается в аксиомах потому шта она естественно правильна ведь там математики все делают на рефлексах и не могут ошибаться. А конпункторы у них хоть и рефлексов нет но они там что то вычисляют а раз оно что то там вычисляет значит у утверждения есть ВЫЧИСЛИТЕЛЬНЫЙ СМЫСЛ следовательно оно не может быть не верным. Как то так. Посмеши деда еще. Можешь про неформализуемость алгоритма ведь ТУЮРИНГ ПРОБЛЕМА ОСТАНОВА ГРОБ ЧЕРВЬ ПИДОР в своем манямирке спиздануть, очень потешно.
Аноним 09/11/19 Суб 14:02:28 151685284
>>1516748
>Вон тебе бумажка, сам выписывай. Я ебал такой хуйнёй заниматься.
Боишься в 4,523,659,424,929 символов не уложиться что ли?
>До чего ты доебался, петух?
Хочу понять почему 0 ≠ 1, да что то рефлексов не хватает. Думал в этом треде мне смогут помочь ((((((
Аноним 09/11/19 Суб 14:06:54 151685485
>>1516852
>Боишься в 4,523,659,424,929 символов не уложиться что ли?
А то.

>Хочу понять почему 0 ≠ 1
Бля, ну если ты этот пруф осилить не можешь, то земля тебе стекловатой, бро.
Аноним 09/11/19 Суб 14:28:09 151686586
>>1516850
Что сказать-то хотел, чучело? Горелым пердаком по всему мейлру трясти у тебя время есть, а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету? Ну кукарекай дальше, если тебе это интереснее, чем хотя бы попытаться разобраться в теме, дело твое. Просто свое место у параши не забывай, твои победоносные кукареканья не делают тебя умнее создателей конструктивной математики, не забывай этот простой факт.
Аноним 09/11/19 Суб 16:42:23 151697987
>>1516854
Как я его осилю если его тупо нет. Как можно осилить то чего нет? Местная пидорва все боится чего то обосраться и делает вид что лениво.
>>1516865
>НИПИЧОТ
Нормас петушка клинит. Главное не забудь на иконы Швятого Браузера и Мартина-Лефа перед сном передернуть.
Аноним 09/11/19 Суб 16:44:49 151698088
>>1516979
>Как я его осилю если его тупо нет
Ты слишком жирный петушок.
Аноним 09/11/19 Суб 16:50:36 151698389
15092119589240.png (226Кб, 1336x839)
1336x839
>>1516850
> Посмеши деда
Говна на обед поел уже, дед?
>>1516979
Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
Аноним 09/11/19 Суб 16:58:39 151698690
Запартная херня для дошколят.
Аноним 09/11/19 Суб 17:17:54 151699291
constru1.png (27Кб, 937x360)
937x360
constru2.png (18Кб, 936x204)
936x204
constru3.png (11Кб, 610x189)
610x189
constru4.png (22Кб, 904x300)
904x300
>>1516983
>Ты в одном разделе уже официально за клована, хочешь здесь успех повторить? Ну ок.
Ты снова проецируешь, конструшила?
Аноним 09/11/19 Суб 17:20:30 151699692
constru5.png (16Кб, 901x223)
901x223
constru6.png (22Кб, 759x378)
759x378
constru7.png (15Кб, 935x220)
935x220
constru8.png (26Кб, 937x283)
937x283
Аноним 09/11/19 Суб 17:21:40 151699893
constru9.png (40Кб, 945x372)
945x372
constru10.png (24Кб, 666x432)
666x432
constru11.png (83Кб, 931x687)
931x687
constru12.png (23Кб, 942x271)
942x271
Аноним 09/11/19 Суб 17:23:15 151700194
constru13.png (36Кб, 938x262)
938x262
constructuhnach[...].png (16Кб, 582x210)
582x210
cube.png (66Кб, 938x569)
938x569
voevod.png (36Кб, 951x522)
951x522
Аноним 09/11/19 Суб 17:45:40 151703095
Аноним 09/11/19 Суб 17:49:19 151703296
>>1517030
Продолжай убеждать себя в этом конструшок.
Аноним 09/11/19 Суб 18:07:15 151704597
>>1516752
Если кратко то Lean is a new Coq.
Аноним 09/11/19 Суб 18:25:22 151705798
>>1517032
>МАМА У МЕНЯ ЖОПА НЕ ГОРИТ ПОВТОРЯЮ НЕ ГОРИТ
Аноним 09/11/19 Суб 18:33:43 151706499
Аноним 09/11/19 Суб 18:38:50 1517069100
>>1516865
>а осилить чем в конструктивной математике аксиома отличается от правила вывода с непустыми посылками, или что такое изоморфизм Карри-Говарда, нету?
Я кстати пытаюсь почитывать швятые писания, удерживая рвотные порывы, но таких "вершин" как конструктух мне никогда не достичь, потому что - паста
> понятно только ебанутым ... подобно тому, например, как христианам понятно как женщина была сделана из ребра мужчины, в то время как ни один нормальный человек такой хуйни никогда не поймёт просто потому что он нормален, а не ебанут
Аноним 09/11/19 Суб 18:57:26 1517078101
>>1517069
В чем цель всех этих твоих потуг, пидорша? Что и кому ты хочешь доказать?
Аноним 09/11/19 Суб 19:01:09 1517079102
>>1517078
Думал, что так просто натянуть на хуй программистов, но программисты оказались смышлёней него.
Аноним 09/11/19 Суб 19:29:36 1517098103
>>1517064
Если длинно, то Coq всегда был фреймворком для разработки тактик с удобным сопряжением со внешним миром. Lean в этом смысле более народный из-за С++ и в то же время более быстрый. В отличии от Coq, у Lean достаточно простое и понятное ядро, гораздо легче писать тактики, не нужно учить ocamlp5 и 4 промежуточных языка для этого. В Lean вкатаны уже достаточно интересные вещи типа перфектоид пространств, а все что вы можете найти на коке это либо старье либо как когда-то писали деды.
Аноним 09/11/19 Суб 19:32:17 1517102104
>>1517098
4-я версия Lean уже будет обладать макросистемой и self-hosting, поддерживать FFI в С/C++, можно будет писать свои веб сервера, консольные приложения, и проганять ваши теории на промышленных датасетах прямо в производстве на полях.
Аноним 09/11/19 Суб 19:47:40 1517126105
>>1517078
Тебе срачелу разворотить например. Вижу что результат весьма неплох.
>>1517079
Хороший самоподдув
>>1517102
>4-я версия Lean уже будет обладать макросистемой и self-hosting, поддерживать FFI в С/C++, можно будет писать свои веб сервера, консольные приложения, и проганять ваши теории на промышленных датасетах прямо в производстве на полях.
>СУПЕРКОМПЬЮТЕРЫ БУДУТ РАЗМЕРОМ С ТЕЛЕФОН, ТЕЛЕФОН С ИНТЕГРАЛЬНУЮ СХЕМУ, ИНТЕГРАЛЬНАЯ СХЕМА С НАНОРОБОТА, А НАНОРОБОТЫ В КАЖДОМ ПРЕДМЕТЕ БУДУТ СИДЕТЬ И ПЕРЕСТРАИВАТЬ МАТЕРИЮ НА СУБАТОМНОМ УРОВНЕ!
Ага и обратная совместимость по пизде пойдет и все
>интересные вещи типа перфектоид пространств
по пизде пойдут
Аноним 09/11/19 Суб 19:51:35 1517132106
>>1517098
>и в то же время более быстрый
Неужели прямо из MSR подвачевываешь? Мое почтение. Какой же невероятный пиздеж
Аноним 09/11/19 Суб 19:59:21 1517142107
>>1517126
>по пизде пойдут
Обещают режим совместимости со старым синтаксисом.
Да и всё равно перепишут.
Аноним 09/11/19 Суб 20:41:35 1517186108
>>1517132
Что, есть сомнения, что С++ тактики быстрее OCaml?
Аноним 10/11/19 Вск 12:03:41 1517599109
Аноним 10/11/19 Вск 12:53:50 1517629110
>>1512674 (OP)
Кто-нибудь знает, x86 ISA верифицирована? Как там с доказанной корректностью процессоров, вообще?
Аноним 10/11/19 Вск 18:18:24 1517937111
>>1517629
Конечно все процессоры верифицированы уже.
486 верицифировали на ACL2, пентиумы уже на проприетарных чекерах.
Аноним 10/11/19 Вск 18:30:32 1517945112
Аноним 11/11/19 Пнд 05:01:38 1518384113
>>1517937
Почему в верифицированной архитектуре могут возникать ошибки (как с FDIV в Пентиумах) или уязвимости как Meltdown или Spectre?

>проприетарных
То есть исходники закрыты? И как тогда проверить доказательство ИХ корректности?

>>1517945
А сами эти чекеры на x86 работают?
Аноним 13/11/19 Срд 05:54:56 1519870114
Будущее программного обеспечения это верифицированный софт и аппаратные средства. Представьте себе ИИ, недружественный к людишкам. Он без проблем найдет миллионы дыр в поделиях от индусских соевых анальников. И все, пизда. Единственный выход - сворачивать все эти хипстерские яп, разгонять ссаными тряпками дармоедов с петушиными андеркатами из барбишопа, всех этих зумеров вкатывальщиков и прочее быдло.
Аноним 13/11/19 Срд 07:52:29 1519881115
>>1519870
>маняфантазии борщехлёба
Аноним 13/11/19 Срд 10:57:17 1519930116
>>1519870
Дефект по типу «второй жизни» определяется тотальными странностями, распространяющимися на все сферы психической деятельности: эксцентричность внешности и речи, парадоксальность и дефицитарность эмоциональной сферы, достигающие степени регрессивной синтонности отношения с окружающими, полностью замещающие профессиональную деятельность аутистические сверхценные увлечения, – и сочетается с психопатоподобными расстройствами иного круга (зависимые, истерические) и псевдоорганическими/астеническими нарушениями.

При этом происходит переосмысление и ревизия системы ценностей, прежде всего относящихся к конвенциональной деятельности: прежние, социально значимые интересы (учеба/работа) отчуждаются и обесцениваются, подменяясь патологическими сверхценными увлечениями

Основным содержанием жизни (сверхценное мировоззрение при изменениях типа фершробен [Аведисова А.С., 1988; Birnbaum K., 1906]), становятся «патологические сверхценные увлечения» [Сергеев И.И., Малиночка С.А., 2008] с идеями реформаторства или собирательства – странные, оторванные от реальности хобби, выступающие в качестве проявлений односторонней аутистической активности и носящие характер необычных, подчас лишенных всякого смысла, не приносящих дохода увлечений
Аноним 13/11/19 Срд 11:58:50 1519955117
У борщехлебов очевидный фершробен, лол.
Аутизм - чек, нездоровые отношения с коллегами - чек, двойная жизнь - чек. В жизни это крудошлеп, боящийся сокращения, который 24/7 разгребает таски, а на двачах это успешный технофилософ каратель анальников.
Аноним 13/11/19 Срд 12:02:09 1519959118
>>1515944
>Дерево вывода покажи
И покрути
Аноним 13/11/19 Срд 12:49:14 1519991119
Аноним 13/11/19 Срд 15:27:41 1520111120
>>1516035
>Да нормальный синтаксис, быстро привыкаешь.
В dlang скобки шаблонов <> даже выкинули чтобы лишний раз не заставлять шифт нажимать, а ты в 2019 предлагаешь такое нормой
Аноним 14/11/19 Чтв 00:22:25 1520537121
>>1519930
Такое можно про любого увлеченного человека сказать. Охуеть, наука уровня астрологии.
Аноним 14/11/19 Чтв 00:26:44 1520543122
>>1517186
Оба языка считаются "быстрыми", так что все зависит от криворукости писавших. Можно даже допустить что что-то там на lean работает быстрее и какое-нибудь мега-доказательство будет верифицироваться на lean всего два машино-месяца вместо четырех на coq. Вот только мне от этого совсем не легче когда я запускаю lean и оно у меня моментально отжирает гигабайты памяти, грузит проц на все сто и падает.
14/11/19 Чтв 02:55:39 1520584123
>>1519930
>Малиночка
хех ну вы лалки
Аноним 16/11/19 Суб 07:19:26 1522382124
>>1520111
Зачем для набора «\» шифт?
Почему тебе лень нажать шифт?
Аноним 16/11/19 Суб 08:18:38 1522406125
>>1522382
Начинать все ключевые слова с какого-то спецсимвола это и правда не от мира сего решение. Видно, что умы авторов языка пребывают в каком-то астрале, слабо связанным с такими земными вещами, как клавиатуры, глаза, эстетика.
Аноним 16/11/19 Суб 09:24:50 1522415126
>>1522406
>Начинать все ключевые слова с какого-то спецсимвола
В чём проблема‐то? Это расширяет диапазон допустимых имён для определений. В лишпе вон скобка на скобке, но никто не кукарекает, что это не от мира сего язык.
Аноним 17/11/19 Вск 07:00:43 1523043127
>>1522415
кукарекают кукарекают
Аноним 17/11/19 Вск 09:50:57 1523067128
>>1522415
>В лишпе вон скобка на скобке, но никто не кукарекает, что это не от мира сего язык.
Ессно - лисп мёртв, его дрочат два с половиной ебаната
Аноним 17/11/19 Вск 09:56:16 1523069129
Язык APL вообще специальную клавиатуру требовал
Аноним 17/11/19 Вск 12:48:09 1523118130
>>1522406
> Видно, что умы авторов языка пребывают в каком-то астрале, слабо связанным с такими земными вещами, как клавиатуры, глаза, эстетика.
Суть этих языков не в том, чтобы наиндусить как можно больше говнокода. Задача нотации - быть максимально прозрачной и близкой к общепринятой математической, для чего в той же агде поддержка юникода https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html
Аноним 17/11/19 Вск 17:31:26 1523398131
>>1523118
ну этот бекслеш в кубике джетбрейнса по началу тоже заебывал, но потом привык. Если Кнуту можно в TeX то и Исаеву тоже!
Аноним 18/11/19 Пнд 02:22:38 1523800132
>>1523118
>Суть этих языков не в том, чтобы наиндусить как можно больше говнокода.
Так и про брейнфак можно сказать.
>Задача нотации - быть максимально прозрачной и близкой к общепринятой математической
И как в этом помогает \where?
Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Аноним 18/11/19 Пнд 15:11:45 1524010133
>>1523800
Что значит «слишком сложен»? Я привел характеристики языков по значимому для меня набору критериев. Я осознаю, что существуют безмозглые пидоры, у которых в список значимых кримериев может входить, к примеру, синтаксис языка. Hу так накласть мне на них. Меня интересуют объективные критерии, а не цацки всякие.

(с) vsl
21/11/19 Чтв 23:12:10 1526300134
>>1523800
>Если у людей отсутствует какое-либо представление о читаемости, удобстве, красоте, то как можно серьезно относиться к их попыткам в языки? В своих формальных системах они тоже нагородили чуши и говнокода, я это гарантирую даже не глядя на их поделия.
Просто два чая этому любителю прекрасного.
Аноним 05/12/19 Чтв 14:57:49 1538243135
Бамп.
Аноним 28/12/19 Суб 13:25:42 1559500136
Предновогодний бамп.
28/12/19 Суб 17:01:02 1559676137
>>1512674 (OP)
Вроде бы скрываешь треды, а через некоторое время, когда они почти утонули, кто-то их бампает, и они опять появляются. Почему так?
Аноним 28/12/19 Суб 20:21:39 1559889138
>>1559676
Потому что ты хуй, а это лучший тред во всем /pr/
Аноним 28/12/19 Суб 22:39:59 1559955139
>>1559889
Настолько лучший, что его даже бампать бесполезно?
Аноним 28/12/19 Суб 23:29:29 1559988140
Аноним 29/12/19 Вск 07:58:01 1560112141
1569950921loope[...].mp4 (3479Кб, 1280x960, 00:00:19)
1280x960
Аноним 16/01/20 Чтв 16:43:52 1574321142
https://github.com/ice1000

Что это за азиатский монстр? Как столько всего можно знать в 19 лет? В 16, судя по коммитам он уже спокойно вертел avl деревья, пилил свои компиляторы и свободно владел парой десятков языках, ТК он также отлично знает, а сейчас устроился на позицию пруф чекера в жидбрейнс. Он гений или просто убер-задрот? Или всё вместе?
Аноним 16/01/20 Чтв 16:47:09 1574325143
>>1574321
Поправка: не теорем пруфера, а разработчика тулзов для теорем пруферов. Наверное доведёт arend до ума.
Аноним 16/01/20 Чтв 21:57:00 1574637144
>>1574321
Если несколько лет дрочить все это по 6 часов в день, вместо хождения в говновуз, сидя на шее у родителей, то почему нет.
Олсо, где ты там его возраст нашел?
Аноним 17/01/20 Птн 01:26:56 1575034145
Аноним 18/01/20 Суб 03:23:10 1576165146
>>1574321
нормальный штрих, урененный средний уровень хорошего мирового инженера!
Аноним 28/01/20 Втр 20:06:19 1585052147
Аноним 09/02/20 Вск 20:46:40 1596614148
Поясните за Идрис, подходит ли для прикладного программирования, или если не теорем пруверами заниматься то лучше не лезть?
Аноним 09/02/20 Вск 20:52:19 1596621149
>>1596614
> подходит ли для прикладного программирования
Нет. /thread
Аноним 10/02/20 Пнд 19:11:07 1597444150
>>1596614
>прикладного программирования
Ты ещё заработать предложи.
Аноним 10/02/20 Пнд 20:20:05 1597494151
>>1596614
Идрис говно из жопы, бери Агдочьку
Аноним 13/02/20 Чтв 03:04:35 1599968152
>>1597494
согласен со всеми господинами!
Аноним 13/02/20 Чтв 04:39:39 1600009153
image.png (1277Кб, 1080x717)
1080x717
Сереженька, бегом на кухню! Я борщик приготовила вкусный! Щавлевый!
Аноним 13/02/20 Чтв 12:06:36 1600154154
Аноним 13/02/20 Чтв 23:16:20 1600971155
>>1512674 (OP)
А какая практическая польза ото всего этого?
Аноним 13/02/20 Чтв 23:20:38 1600975156
>>1600971
Какие ссаные тряпки надо сувать в ОП-пост, чтобы вас тут не было?
Аноним 13/02/20 Чтв 23:28:09 1600986157
>>1600975
Достаточно прекратить страдать бесполезной хуйнёй, а в кои-то веки выучить пхп и жс.
Аноним 13/02/20 Чтв 23:28:26 1600987158
>>1600975
Те, которые ты намотал на себя
Аноним 13/02/20 Чтв 23:36:36 1600999159
>>1600986
Зачем? У нас есть jscoq!
Аноним 13/02/20 Чтв 23:50:05 1601024160
>>1600999
Если будет oraclecoq, то я с вами крч.
Аноним 19/02/20 Срд 06:58:58 1607439161
>>1601024
вообще-то пруверы в ИТ притащили именно для того, чтобы не получались такие поеботы как Ораклы больше никогда в индустрии.
Аноним 25/02/20 Втр 17:30:23 1614800162
image.png (53Кб, 549x307)
549x307
Аноним 25/02/20 Втр 19:12:06 1614887163
553.png (752Кб, 796x768)
796x768
>>1614800
Вот не надо тут нам этого
Аноним 25/02/20 Втр 23:53:31 1615096164
image.png (9Кб, 497x247)
497x247
Аноним 25/02/20 Втр 23:59:53 1615102165
Аноним 26/02/20 Срд 00:05:00 1615110166
>>1615102
Это другие, неправильные классы.
Аноним 26/02/20 Срд 00:18:50 1615121167
Аноним 26/02/20 Срд 00:20:39 1615125168
1.png (147Кб, 636x657)
636x657
Аноним 26/02/20 Срд 00:21:01 1615126169
>>1615121
Ты слишком серьёзен. Лучше б что-нибудь доказал
Аноним 26/02/20 Срд 00:28:46 1615130170
>>1615121
> vs
Будто у них что-то общее, кроме названия.
Аноним 26/02/20 Срд 00:30:45 1615132171
Зачем вы это учите?
26/02/20 Срд 00:32:20 1615134172
1.png (147Кб, 636x657)
636x657
>>1615132
СПРОСИ В СВОЕЙ КОНФЕ РАКОУЕБИЩЕ
Аноним 26/02/20 Срд 00:40:20 1615140173
>>1615134
Мне сказали, что это филиал асилума а ты тут главный петух-газонюх.
Попукал вам в тред.
Аноним 07/03/20 Суб 12:03:03 1626075174
Бамп.
Аноним 07/03/20 Суб 12:15:33 1626089175
Чо скажете за dafny?
Аноним 07/03/20 Суб 16:27:49 1626371176
>>1626089
Это же refinement types, то есть не прувер.
Аноним 07/03/20 Суб 17:08:26 1626418177
>>1626089
Зачем тебе эта хуйня без практических задач, лучше питон возьми.
Аноним 09/03/20 Пнд 17:52:41 1628705178
>>1626418
Держать питон прикольно первые десять минут.
Аноним 09/03/20 Пнд 23:57:37 1629081179
Кто с TLA+ имел дело?
Toolbox медленный и работает коряво, например иногда курсор перескакивает куда попало, что меня несколько раздражает — есть ли ему достойные альтернативы?
Аноним 19/03/20 Чтв 17:14:21 1637211180
>>1615102
>>1615110

Ну как в СССР. Были два класса, рабочие и бюрократы. Но это не считается, это другое)))
Аноним 19/03/20 Чтв 17:25:12 1637220181
>>1637211
А ещё классы есть в шкалке. Возвращаешься иакой из шкалки и пишешь тайпклассы.
Аноним 19/03/20 Чтв 22:59:12 1637512182
Аноним 23/03/20 Пнд 08:43:10 1640485183
Поясните за пруверы подробно человеку, который когда-то занимался математикой. Я правильно понял, что это просто движок, который умеет делать преобразования на языке мат.логики, и может размотать изначальное выражение и проверить, приходит ли оно к тому, что надо доказать? Хорошо, а насколько эти движки скилловые? В смысле, мат.логика - это далеко не все. В процессе доказательства привлекаются самые разнообразные методы, в том числе и прямые математические расчеты(выражения и их численные значения), и различные продвинутые методы, даже иногда графические. Я уже молчу о том, что эти движки нужно постоянно обновлять, поскольку постоянно придумываются новые методы и новые области математики. Та же теорема Ферма, доказанная через эллиптические кривые - никому ведь ранее даже в голову не приходило связать одно с другим.
Аноним 23/03/20 Пнд 12:17:54 1640582184
>>1640485
Единственное что этот язык не может, это работу тебе дать)))
Аноним 24/03/20 Втр 21:39:06 1642010185
>>1640582
Работа есть, дело в другом: слишком большой порог вхождения и нужно разбираться буквально во всём в CS, что бы что-то делать полезное.
24/03/20 Втр 22:18:53 1642053186
>>1512674 (OP)
Ссаный тред подёнщиков, которым никогда не откроются тайны бездонного моря алгебраической геометрии.
Аноним 25/03/20 Срд 04:54:08 1642231187
Аноним 25/03/20 Срд 16:09:20 1642532188
Зачем?
Аноним 25/03/20 Срд 16:12:27 1642536189
25/03/20 Срд 17:03:25 1642570190
Аноним 25/03/20 Срд 17:15:16 1642576191
>>1642570
Потому что нам никогда не откроются тайны бездонного моря алгебраической геометрии, а так хоть что-то.
Аноним 25/03/20 Срд 21:10:23 1642776192
quote-mathemati[...].jpg (51Кб, 850x400)
850x400
>>1640485
> Я правильно понял, что это просто движок, который умеет делать преобразования на языке мат.логики, и может размотать изначальное выражение и проверить, приходит ли оно к тому, что надо доказать?
Как-то так, да. Ибо пикрелейтед.
> насколько эти движки скилловые? В смысле, мат.логика - это далеко не все.
Даже йогурты не все одинаково полезны, про матлогику и говорить нечего. Но касаемо HoTT и CuTT - это как раз правильное направление матлогики, про которую нельзя сказать, что она "далеко не все".
> В процессе доказательства привлекаются самые разнообразные методы, в том числе и прямые математические расчеты(выражения и их численные значения), и различные продвинутые методы, даже иногда графические.
Все это (и не только это) тривиально сводится к типам.
> Та же теорема Ферма, доказанная через эллиптические кривые - никому ведь ранее даже в голову не приходило связать одно с другим.
Эллиптические кривые - всего лишь тип в инфинити групоиде, изоморфных которому там полно. В том числе таких, использовать которые в доказательстве теоремы Ферма никогда не придет в голову вообще никому и никогда, потому что мозгов не хватит.
Аноним 27/03/20 Птн 07:24:45 1643680193
1.png (27Кб, 472x304)
472x304
Добавте в шапку треда конфу
Аноним 27/03/20 Птн 08:09:51 1643689194
>>1643680
>Хцдевс
Эта та конфа для фронтендеров-шизиков?
Аноним 27/03/20 Птн 14:46:40 1643930195
>>1643680
Там вообще новости какие-то обсуждают, и говно бесполезное не учат.
Аноним 28/03/20 Суб 00:32:21 1644266196
Аноним 28/03/20 Суб 01:14:49 1644289197
>>1644266
Берёшь и без задней мысли прикручиваешь
По хаскелю и коммон лиспу должно быть больше гайдов, можешь погуглить сначала их
Аноним 28/03/20 Суб 02:19:55 1644309198
>>1644266
Даже к жабаскрипту прикручивают вовсю. Просто берется нужная логика (например, PTS) и пишется на интересующем яп.
Аноним 28/03/20 Суб 23:15:23 1644991199
>>1512674 (OP)
Настоящие математики-профессионалы ссут на вашу теорию типов
Аноним 30/03/20 Пнд 11:05:40 1646055200
Надеюсь в этих ваших пруверах
(sqrt(2) == 1.4142135623730951) == false
Иначе говно без задач.
Аноним 30/03/20 Пнд 15:40:06 1646231201
>>1646055
>1.4142135623730951
Главное чтобы прувер стек оверфлоу не словил, а так всё нормально.

Даже так можно codewars com /kata/5d2b89d4b90c0a001f4a6456
Аноним 04/04/20 Суб 21:07:07 1650266202
>>1644991
это неправда, так как я видел математиков профессионалов, которые занимаются физикой и создают модальную HoTT для своих нужд
Аноним 14/04/20 Втр 09:39:03 1657528203
>>1512717
> реально написать
This.
Аноним 20/04/20 Пнд 16:43:44 1663057204
image.png (36Кб, 626x344)
626x344
Аноним 21/04/20 Втр 22:47:53 1664077205
>>1663057
Дело в том, что √2 никак не может равняться 1.4142135623730951. В математически точных языках редуцируются только редексы(√2 не есть редекс). В математиматически точных языках выражения фактически равняются числам. Т.е √2 это число. Как и ⅓, к примеру.
Аноним 22/04/20 Срд 15:20:45 1664476206
>>1646055
Ни это
1414213562370951 / 1000000000000000
(1414213562370951 / 1000000000000000) = 2
Ни это
1414213562370951
1414213562370951 <> 2 1000000000000000 1000000000000000
/\
1000000000000000 <> 0.

Ванильный петушара не может.
А сделать его неванильным не могу я.
Аноним 22/04/20 Срд 15:21:51 1664479207
>>1664476
1414213562370951 / 1000000000000000 x
(1414213562370951 / 1000000000000000) = 2

1414213562370951 x 1414213562370951 <> 2 x 1000000000000000 x 1000000000000000

Multiplication fix.
Аноним 24/04/20 Птн 12:19:25 1666263208
Аноним 30/04/20 Чтв 00:46:33 1672017209
Аноним 30/04/20 Чтв 02:30:22 1672061210
>>1672017
Продалжаю писать в свой личный тред.

Доказал:
Lemma sqrt2: forall x y,
(0 < x)%nat -> (0 < y)%nat ->
INR x / INR y <> sqrt 2.

Довольно урчу.
Аноним 30/04/20 Чтв 03:15:50 1672068211
>>1672061
Где доказательство?
Аноним 30/04/20 Чтв 03:47:41 1672078212
Аноним 30/04/20 Чтв 22:23:16 1672953213
Аноним 01/05/20 Птн 03:02:17 1673286214
>>1642776
>Эллиптические кривые - всего лишь тип в инфинити групоиде, изоморфных которому там полно
Типа смотришь такой на картину Рембранта: картина это просто краски и холст, краски можно выбрать любые и холст любой.
Аноним 01/05/20 Птн 03:15:25 1673287215
>>1515127
HoTT все дальше и дальше от математики, после того как помер единственный математик у его основ. Уже бизнес кабаны подхватили.
Аноним 01/05/20 Птн 14:43:32 1673556216
>>1672953
>freek
Да я понимаю, что это аутизм, но зачем так грубо.
Аноним 01/05/20 Птн 17:48:11 1673791217
>>1673287
Как я вкатился в НоТТ на 350к/месяц. Топ 20 вопросов на собеседовании по НоТТ. Скидка 50% на курс "НоТТ с нуля" .
Аноним 05/05/20 Втр 14:42:30 1677491218
>>1515428
школота с идрисом съебитесь нахуй
Аноним 05/05/20 Втр 15:55:24 1677629219
>>1677491
А что с идрисом не так?
мимо
Аноним 05/05/20 Втр 19:16:42 1677982220
>>1677629
слоение хопфа запиши на идрисе
Аноним 05/05/20 Втр 21:00:37 1678145221
Аноним 05/05/20 Втр 21:34:39 1678176222
>>1512674 (OP)
Очень интересная аутистская ерунда! Какую самую сложную теорему вы формализовали? Или доказали? Я просто еще не до конца понял, что тут происходит.
Аноним 05/05/20 Втр 21:43:05 1678190223
Аноним 05/05/20 Втр 22:29:02 1678239224
>>1678176
тут в /pr передержка для второгодников, они выписали гомотопические пруверы и рядом Идрис написали. Непонятно что одни доказывают, но вот видно IEEE754, умножение и равенство. В принципе с помощью Идриса больше ничего и не докажешь.
Аноним 05/05/20 Втр 22:32:36 1678244225
>>1677629
Идрис не прувер, в нем можно доказать bottom, нет контроля рекурсии, нет гомотопий, нет ничего, он экстрактит Си программы которые линкуюутся с stdlib и которые текут. Идрис для шотландских бомжей из ПТУ Святого Андрея.
Аноним 12/05/20 Втр 11:17:34 1684813226
идрис говно и моча
Аноним 20/05/20 Срд 21:24:54 1695549227
пынямаешь.png (1301Кб, 1748x985)
1748x985
Идрис2 теперь работает без установленного первого идриса! Собственно, для установке нужен chez scheme.
https://github.com/idris-lang/Idris2
Аноним 20/05/20 Срд 21:27:46 1695551228
>>1678244
> Идрис для шотландских бомжей из ПТУ Святого Андрея.
Идрис - первый в мире ЯП общего назначения на основе зависимых типов. Верифицированный код это будущее программирования в принципе.
Аноним 22/05/20 Птн 00:35:04 1697084229
>>1695549
Зачем идрис компилируется в схему? llvm бэкенд планируется?
Аноним 22/05/20 Птн 04:32:12 1697197230
>>1695551
Но это было будущее 20 лет назад. Оно плавно стало прошлым, так и не пройдя стадию настоящего.
Аноним 22/05/20 Птн 06:42:38 1697207231
>>1697084
> llvm бэкенд планируется?
Можно в С скомпилировать, а из него clang'ом в LLVM.
>>1697197
> Но это было будущее 20 лет назад. Оно плавно стало прошлым, так и не пройдя стадию настоящего.
Манямир. 20 лет назад про зависимые типы знали полтора математика из coq комьюнити. На идрисе сейчас обкатывается то, что в яп будет нормой лет через 10 минимум.
Аноним 22/05/20 Птн 13:28:15 1697590232
>>1697207
>Можно в С скомпилировать, а из него clang'ом в LLVM.
idris -> scheme -> c -> llvm ir -> object code
Охуительно. Толку от верифицированного кода, который проходит через все эти фазы трансляции, обогащаясь низкоуровневыми багами и даже логическими ошибками?
Аноним 22/05/20 Птн 13:59:34 1697619233
155723236711742[...].jpg (46Кб, 720x456)
720x456
>>1697590
> idris -> c -> llvm ir -> object code
Поправил.
> Охуительно. Толку от верифицированного кода, который проходит через все эти фазы трансляции, обогащаясь низкоуровневыми багами и даже логическими ошибками?
Тогда так:
idris -> c -> compcert -> object code. Я думал, тебе именно LLVM нужен, а если просто чтобы было, то пикрелейтед. Опять же, надо пынимать, что Идрис это во многом полигон для обкатки вещей, в программировании общего назначения принципиально новых. Там вон у самого Брэди ошибки при установке, сам себе issues открывает один за одним. Ты хочешь чтобы снихуя все сразу работало, так не бывает. Авиация началась с того что братья Райт на своем поделии три метра пролетели. Ну и там есть механизм запиливания собственных бэкендов.
25/05/20 Пнд 11:47:27 1701371234
[code]
test
[/code]
Аноним 06/07/20 Пнд 21:57:18 1743441235
Ну дык че там, доказатели? Как светлое будущее?
Аноним 09/07/20 Чтв 18:57:49 1746230236
>>1743441
Доказали что его не будет.
Аноним 09/07/20 Чтв 18:58:39 1746233237
>>1746230
Светлого? Или будущего?
Аноним 09/07/20 Чтв 21:29:37 1746353238
А почему нет таких работ, когда какой-нибудь аутист в качестве хобби формализует в одной из этих систем сложное, знаменитое доказательство? Последней теоремы Ферма, например, или чего-то такого.
Делают же люди дома из спичек, яхты в бутылках, модели Звезды Смерти, годами. А это чем хуже? Еще элитнее же выходит, не для быдла - должно быть привлекательно.
Аноним 09/07/20 Чтв 21:35:14 1746357239
>>1746353
Из спичек ты хотя бы можешь подержать в руках, сфоткать и кому-нибудь показать, поставить на полку. А абстрактный выхлоп в консольке никому не интересен, поэтому даже если кто-то этим реально занимается, известно это будет почти никому.
Аноним 10/07/20 Птн 00:08:07 1746486240
>>1746357
Популярность все это действо в целом какую-то имеет. Уже лет 20, если не 30, существуют норм пруверы. Постоянно делаются новые тулзы.
Даже ИТТ видно, что формальные методы привлекательны для некоторой прослойки задротов.
А самих доказательств, если рассматривать сложные теоремы за пределами школьного курса - пересчитать по пальцам одной руки старого фрезеровщика. Никто не копается углубленно, получается. Так, поверхностно поиграют с системой, и бросают. Недаром ИТТ (или в прошлом треде, не помню) большая часть постов была про установку и настройку редактора, лол. Такое впечатление, что на этом все и заканчивается.
Аноним 10/07/20 Птн 01:01:13 1746512241
>>1746486
Просто это действительно сложно. Высшая математика-то доступна меньшинству людей, доказательство теоремы Ферма - так вообще единицам. А этот человек ещё и пруверами должен увлекаться на серьёзном уровне.
Аноним 10/07/20 Птн 01:52:50 1746523242
>>1746353
Если ты знаешь математику, то тебе такая хуйня неособо интересна. Если не знаешь, то доказывать будешь школьное говно.
Аноним 10/07/20 Птн 03:34:01 1746542243
>>1746512>>1746523
А там правда нужно прям знать математику? Если доказательство уже расписано где-то словами, то мне кажется больше инженерная, механическая работа. Раскопать определения, записать их на формальном языке, заполнить пробелы в доказательствах, закодить какие-то стандартные приемы. Ну то есть знать на университетском уровне надо, конечно, но прям чтобы математиком быть - сомневаюсь.
Аноним 10/07/20 Птн 04:15:32 1746550244
>>1746542
> Раскопать определения
> заполнить пробелы в доказательствах
> закодить какие-то стандартные приемы
То есть прошариться до уровня математика в этих рамках. Хуй ты что заполнишь или закодишь стандартные приёмы, если не понимаешь, что и почему происходит.
Аноним 10/07/20 Птн 17:35:36 1747168245
6c3e0a666b151d3[...].png (180Кб, 1919x1079)
1919x1079
>>1746523
>то доказывать будешь школьное говно.
А мне норм.

Кстати, чому пруверам на учат в школе?
Аноним 10/07/20 Птн 20:07:58 1747272246
haskell.jpg (246Кб, 1024x768)
1024x768
>>1512719
>Наш язык для просветленных социалистов, а не потребителей
Аноним 10/07/20 Птн 23:55:56 1747529247
>>1747168
>Кстати, чому пруверам на учат в школе?
А кто учить то будет?
Аноним 11/07/20 Суб 06:45:08 1747728248
>>1747168
Чет хохотнул, представив как средний школьник (АУЕ быдлан с потухшими глазами и гниющими от крокодила руками, из математики с трудом освоивший только сложение на пальцах в 15 лет) пыхтит над доказательством теоремы Пифагора в коке.
Аноним 11/07/20 Суб 13:12:50 1747939249
>>1747728
>средний школьник (АУЕ быдлан с потухшими глазами и гниющими от крокодила руками, из математики с трудом освоивший только сложение на пальцах в 15 лет)
Я имел в виду не ебеня Казахстана, а нормальные ДС-школы, не обязательно 57, но что-то более-менее приличное.
Аноним 11/07/20 Суб 13:35:39 1747970250
>>1747939
>что-то более-менее приличное.
Ну так гниющие, а не сгнившие. Чо ебало скорчил?
Аноним 11/07/20 Суб 13:44:46 1747989251
Аноним 11/07/20 Суб 13:55:43 1748000252
>>1512674 (OP)
Спрошу тут. А почему программирование не пошло по такому пути? Ну скажем, описываем на некоем языке регистры процессора. Также описываем действия - то есть по сути регистры до, действие, регистры после. (Не только регистры, но и флаги, память, не суть). Потом описываем что должна делать программа (например вывести число на экран). А компьютер уже сам подбирает алгоритм, исходя из того что мы хотим получить (возможно мы задаем хинты, что важнее память или производительность, хотя по идее и это он сам может шедулить). Сам подбирает нужные команды процессора. Какие подводные камни?
Аноним 11/07/20 Суб 14:05:39 1748005253
>>1747989
Чтобы потом доказать на прувере что ты пидор.
Аноним 11/07/20 Суб 16:13:59 1748166254
LISPmachine.jpg (783Кб, 1536x2032)
1536x2032
>>1748000
Да никаких, собственно.
Аноним 11/07/20 Суб 16:49:44 1748240255
>>1748000
То есть описывать не последовательность действий (императивное программирование), а результат (декларативное)?
На практике получается, что результат надо описывать слишком подробно, потому что его надо декомпозировать на подрезультаты, которые, по сути, являются подздадачами, и в конце получается точно такой же императивный код, но вывернутый наизнанку.
Можно сравнить с рецептом, как я писал здесь >>1685842 →

У борщехлёбов другое мнение, но кого оно волнует.
Аноним 11/07/20 Суб 19:56:10 1748440256
>>1748240
>На практике получается, что результат надо описывать слишком подробно
Почему? Пусть компьютер сам оптимально разбивает на декомпозицию.
11/07/20 Суб 20:03:16 1748451257
>>1748240
Тебя недостаточно обоссали в прошлый раз и ты пришёл за добавкой, мудило?
Аноним 11/07/20 Суб 21:17:01 1748535258
>>1748440
Ну как он это сделает? Это всего лишь машина, которая не может сама думать и не может магически влезть в голову программиста, чтоьы понять, чего он хочет. Единственный способ - обернуть простейшие команды в более сложные, их ещё в более сложные, и так далее до привычных процедур. Всё, что можно сделать - немного изменить семантику на самом верхнем уровне, но под капотом будет то же самое.

>>1748451
В тот раз внятных аргументов, кроме РЯЯ ВРЁТИ, я так и не услышал, уверен, что не услышу и сейчас. Поэтому уходи.
Аноним 11/07/20 Суб 22:36:24 1748616259
>>1748535
Шо тут непонятного то? Программист задекларирует, например, что есть команда копировать файл. Опишет что вот у нас диск до выполнения команды, а после выполнения команды диск должен содержать дополнительную копию указанного файла. Что тут мешает компьютеру самому определить, какие действия надо провести, чтобы получить желаемое изменение?
По сути, компилятор для всего. Ведь это то же самое, что делает компилятор, когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение, разве нет?
Аноним 11/07/20 Суб 23:14:44 1748655260
>>1748616
Не совсем понятно, как это должно выглядеть. Так что ли?
исходное_состояние = [файл, ⚹]
прочее = исходное_состояние - файл
новое_состояние = [файл, файл, прочее]
эвм.начать_думать(исходное_состояние, новое_состояние)

Чем-то напоминает пролог. Ты не на него намекаешь? Деталей я не знаю, но, вроде, выяснилось, что он оказался не всесильным и слишком сложным для чего-то реального.

> когда подбирает ассемблерные инструкции со сдвигом, когда в программе на си было написано умножение
Это оптимизация, а не игра в угадайку. Изначально никаких оптимизаций не задумывалось, предполагалось, что как пишет программист, такие инструкции и будут. Оптимизации же появились не чтобы решать задачи за программиста, а чтобы прозрачно для него ускорить работу выполнения кода.
Аноним 12/07/20 Вск 07:26:33 1748819261
>>1748000
> регистры до, действие, регистры после.
>>1748240
>>1748440
>>1748535
Хуя тут авангард мысли. Так и до логики Хоара додумаетесь, а может быть даже и до separation logic. Между прочим, программирование в стиле "дать комплюхтеру задачу, а он пусть сам ебется с ее реализацией", это ровно то, чем занимается например Брэди сотоварищи в рамках type-driven development. Но там пока все очень далеко от идеала, уточнять постановку задачи по ходу дела должен таки человек. К этому же в идрисе столько всяких кодгенов, во втором идрисе, например, третьего дня кодген js запилили. Т.е ты делаешь на идрисе чего тебе надо, а потом компилишь всю хуйню в жс итд.
Аноним 12/07/20 Вск 07:37:44 1748820262
>>1748819
> додумаетесь
Не я, для меня единственное доказательство корректности - тестировщики ничего не нашли, а на проде ни разу не остановились бизнес-процессы.
Аноним 12/07/20 Вск 07:43:14 1748821263
>>1748820
Тестированием можно выявить наличие ошибок, но не доказать их отсутствие. Для всяких кабанчиковых приложений и так сойдёт, конечно же.
Аноним 13/07/20 Пнд 11:57:49 1750046264
>>1748819
Причем тут тройки Хоара? Они нужны только для проверки, а не для создания алгоритмов.

То что он описал, мне больше напомнило proof-search подход по типу LambdaProlog, но там тоже не алгоритм строится, а доказательство выводится.
Аноним 30/07/20 Чтв 08:16:31 1763950265
Аноним 02/08/20 Вск 07:40:02 1766054266
>>1763950
> прувер для metamath
HoTT бы автоматизировали, а метамат этот кому нужен? Там и нейроночки не нужны, записать его в BNF форме и генетические алгоритмы прикрутить, которые к слову, превосходят deepRL в играх атари, грамматической эволюции там более чем достаточно.
Настройки X
Ответить в тред X
15000 [S]
Макс объем: 40Mб, макс кол-во файлов: 4
Кликни/брось файл/ctrl-v
Стикеры X
Избранное / Топ тредов