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

Ответить в тред Ответить в тред
Check this out!
Пруверов тред #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 в играх атари, грамматической эволюции там более чем достаточно.
Аноним 10/09/20 Чтв 05:44:52 1802356267
Аноним 12/10/20 Пнд 16:03:24 1828602268
>>1802356
AI во всём превзошёл анона?
Аноним 12/10/20 Пнд 19:59:50 1828755269
>>1828602
Оно там только пытается доказать теоремы, которые уже были доказаны в метамат. Делает это лучше других доказателей, но результаты все еще не сказать чтобы впечатляют.
Аноним 13/10/20 Втр 12:34:21 1829175270
И че теперь математикам делать, когда их автоматизируют
Аноним 13/10/20 Втр 12:37:14 1829178271
Аноним 13/10/20 Втр 13:40:35 1829227272
>>1829175
Автоматизация доказательств не имеет смысла.
В программировании, даже если код суперуёбищный до такой степени, что никто не понимает как он работает - он всё равно выполняет какую-то функцию, он полезен.
А в математике блекбокс прувер который отвечает да/нет как раз не имеет никакой пользы, потому что в математике важнее "каким образом", "что это значит" и "что это нам даёт", а на такие вопросы манясетки конечно же не ответят, пока что их удел - разгадывать капчу.
Аноним 13/10/20 Втр 17:59:44 1829431273
>>1829227
Что ещё за блекбокс прувер? Прувер, которому нужно верить, потому что он прувер?
Аноним 13/10/20 Втр 19:14:49 1829501274
>>1829227
На эти вопросы ты отвечаешь, когда придымываешь само утверждение. Это отдельная задача от доказательства.
Ну и найс гоалпост мувинг, конечно.
14/10/20 Срд 08:48:20 1829810275
>>1748000
По сути, так работает каждый портируемый оптимизирующий компилятор.
Аноним 14/10/20 Срд 15:01:32 1830150276
16026188995930.gif 391Кб, 652x562
652x562
>>1829227
> Автоматизация доказательств не имеет смысла.
Сказал зумер. Судя по написанному дальше, вообще не понимающий о чем пишет.
Аноним 16/10/20 Птн 22:49:40 1832349277
>>1830150
Потыкал палочкой шизика.
Аноним 20/10/20 Втр 17:45:24 1835526278
>>1832349
Анус себе потыкай. На шизиках мир стоит!
Аноним 20/10/20 Втр 20:38:06 1835632279
>>1835526
Так вот почему мне так тяжело. Уберите мир плес.
Аноним 20/10/20 Втр 21:20:42 1835683280
Аноним 03/11/20 Втр 00:49:42 1846739281
А пределы можно доказывать? Где лучше?
Аноним 06/11/20 Птн 15:37:45 1849615282
>>1846739
Как тут codewars com/collections/mathematical-analysis ? Нахуй тебе это нужно?
Аноним 14/11/20 Суб 16:27:41 1856014283
image.png 131Кб, 1305x506
1305x506
image.png 194Кб, 482x550
482x550
image.png 78Кб, 300x432
300x432
image.png 172Кб, 230x330
230x330
Чем блять это говно на пиках отличается друг от друга, мне кто-нибудь может объяснить?
Аноним 14/11/20 Суб 19:36:25 1856198284
>>1856014
>отличается
Теория описывает методологию интерпритации объектов в определенном фрейме
Магия рун является всего лишь одной из интерпритаций объекта руны
Ну и ты долбаёбушка на правильном пути если начинаешь что-то подозревать
Аноним 14/11/20 Суб 22:08:06 1856314285
>>1856198
Наставь на путь истинный.
Аноним 17/11/20 Втр 12:12:54 1858306286
>>1856314
Тебе не нужен этот путь
Аноним 20/12/20 Вск 11:58:15 1885319287
маскот АГДЫ - официальная курочка

кто теперь агдоводы?
Аноним 20/12/20 Вск 20:44:08 1885659288
>>1885319
Это серьезная проблема. У кока - петух, у агды курочка. Это же кризис индустрии!
Аноним 20/12/20 Вск 21:21:17 1885703289
Аноним 20/12/20 Вск 22:13:33 1885717290
>>1885703
За такие видео надо пермачить.
Аноним 20/12/20 Вск 22:27:36 1885729291
>>1885717
пригорело, конструшок?
Аноним 21/12/20 Пнд 00:27:13 1885779292
>>1856014
тоже не понимаю почему синтаксис нельзя сделать проще
Аноним 21/12/20 Пнд 00:39:59 1885781293
>>1885659
Нет, это повод нести яйца!
Аноним 21/12/20 Пнд 01:26:56 1885787294
Аноним 21/12/20 Пнд 10:01:02 1885958295
>>1885781
Белуга не несет яйца. Переходите на Белугу.
Аноним 21/12/20 Пнд 10:21:28 1885975296
Аноним 21/12/20 Пнд 16:43:09 1886276297
>>1885958
Коки не топчут белуг - не интересно
Аноним 22/12/20 Втр 11:26:05 1886879298
>>1886276
(записывает в блокнотик)
на третий день обсервации госпитализированный пациент продолжает идентифицировать себя с домашней птицей французской породы.
от предложенных рыбных блюд отказался, обосновав это своими сексуальными проблемами.
рекомендации: продолжать наблюдение.
Аноним 23/12/20 Срд 02:22:57 1887695299
>>1886879
>на третий день
Я тут с первого треда подсераю, прояви уважение, ёба
Аноним 24/12/20 Чтв 18:03:22 1889573300
>>1887695
я наблюдаю только три дня, так что прошу извинить
Аноним 24/12/20 Чтв 18:07:58 1889582301
В городе Колпино группа встречает группу буддистов, которых герои берут с собой. В новгородском посёлке Чудово, путники вынуждают сделать остановку. Там они встречают охотника Одноглазого, который от радости приглашает всех к себе в гости. Математик решает остаться следить за составом. На следующий день возвращаются Александр с Владимиром Павловичем, от которых Математик узнаёт, что Одноглазый оказался каннибалом и убил всех буддистов. Команда продолжает путь.

(энциклопедия метро)
Аноним 28/12/20 Пнд 22:52:15 1894044302
>>1889582
> от которых Математик узнаёт
А доказать?
Аноним 29/12/20 Втр 00:45:52 1894146303
Аноним 09/01/21 Суб 00:12:48 1905167304
Чтобы принять, что верифицированное доказательство корректно, нужно быть уверенным в корректности верификатора. И так по всей цепочке до железа, которое работает на физических объектах, точность которых невозможно гарантировать. Приходится верить, что все работает как надо.
Какая тогда принципиальная разница между верифицированным автоматически доказательством и обычным, проверенным вручную?
Аноним 09/01/21 Суб 16:24:56 1905591305
Аноним 09/01/21 Суб 17:00:11 1905620306
>>1905167
Машина ошибается гораздо реже чем человек, и чем сложнее задача, тем больше вероятность ошибка человека. Например попробуй перемножь две матрицы хотя бы 10 на 10 вручную, с огромной вероятностью ты допустишь много ошибок, в то же время компьютер их перемножит за долю секунды абсолютно правильно.
Аноним 09/01/21 Суб 20:31:46 1905875307
>>1905167
Зачем что-то проверять, если могут свет вырубить.
Аноним 09/01/21 Суб 21:03:20 1905928308
>>1905620
Выходит, это все опять же про вероятности. Так это не отличается от принятия доказательств голосованием, как это сейчас делается. Там тоже, чем больше седобородых мудрецов одобрит доказательство, тем оно вернее.
Аноним 10/01/21 Вск 16:37:50 1906552309
>>1905928
Се ля ви, абсолютной истины не существует.
Аноним 10/01/21 Вск 22:17:41 1906895310
>>1905167
>Чтобы принять, что верифицированное доказательство корректно, нужно быть уверенным в корректности верификатора
Как-бы нет, нужно не самого субъекта проверять, а сам объект.
Аноним 11/01/21 Пнд 05:37:29 1907034311
>>1512674 (OP)
Так Idris же вроде язык общего назначения, с элементами прувера.
Аноним 11/01/21 Пнд 12:51:34 1907186312
>>1905167
Для освобождения человека от работы по проверке доказательств вручную
Аноним 20/01/21 Срд 12:31:15 1916162313
image.png 7Кб, 332x307
332x307
Что скажете про model checking, в частности, Spin?
никогда не думал, что напишу сюда
Аноним 20/01/21 Срд 12:32:50 1916164314
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"
Аноним 20/01/21 Срд 12:41:33 1916166315
>>1748535
> Ну как он это сделает? Это всего лишь машина, которая не может сама думать и не может магически влезть в голову программиста, чтоьы понять, чего он хочет.
GPT-3
Аноним 20/01/21 Срд 12:49:25 1916173316
>>1916166
Естественные языки плохо формализуются, да и даже если попытаться, писать пришлось бы ещё больше, чем на языке программирования, ибо человеческие языки громоздки, нерегулярны и с произвольной трактовкой.
Аноним 20/01/21 Срд 12:53:18 1916176317
>>1916173
> GPT-3, сделай имиджборду на vue.js, пусть тема будет оранжевой, а маскотом будет Холо.
O'rly? Думаешь это короткое приложение больше чем исходный код, который сгенирирует GPT на выходе?
Аноним 20/01/21 Срд 13:08:37 1916186318
>>1916176
Это прям-таки всё? Не нужно описывать, что такое имиджборда и vue.js, какие решения принимать по умолчанию для не упомянутых параметров? А если нужно, чем это лучше процедуры generate_imageboard(framefork="vue.js", theme="orange", mascot="Holo") ?
Аноним 20/01/21 Срд 14:46:07 1916266319
>>1916186
> Не нужно описывать, что такое имиджборда и vue.js
Не нужно. Знания об этом уже есть в GPT-3.
> какие решения принимать по умолчанию для не упомянутых параметров?
На усмотрение GPT. Сделает максимально дефолтный вариант.
Аноним 20/01/21 Срд 14:56:31 1916276320
>>1916266
Звучит круто. Раньше натыкался только на проект, где по словесному описанию рисовалась картинка, работало, вроде, на нейронках.
Аноним 20/01/21 Срд 15:10:46 1916283321
>>1916276
Ты про DALL-E? Он также работает в связке с GPT-3. Сейчас возможности GPT-3 по программированию ограниченны, но это только потому что в датасет не были включены сорсы из гитхаба. Как только будет выкачен GPT-4 (надеюсь, с гитхабом), GPT-3 станет не просто мощнейшим инструментом программиста, он сможет заменить его end-to-end в большинстве задач, связанных с айти: написание сайтика, поиск багов, тайпчекинг, написание компиляторов, любых программ, на любом языке программирования. И кроме всего прочего, сделает тебе красивую md-документацию для сгенерированного кода.

Мы на пороге революции.
Аноним 20/01/21 Срд 15:40:35 1916306322
>>1916283
> DALL-E
Возможно. Не помню, давно читал тот пост где-то.
> Мы на пороге революции
Ждём.
Аноним 22/01/21 Птн 20:12:38 1918327323
>>1747168
Сверстанный текст на ЛаТеХе выдают за код (неведомого) прувера?
Аноним 24/01/21 Вск 09:50:17 1919740324
>>1905167
>>1905928
Ты не понимаешь, о чем пишешь. 1+1=2 безотносительно того, отключат свет или нет. То же самое с любыми правилами построения в прувере. А вот горький петух со своим форсом гпт3+ вполне может оказаться прав, итеративный файнтюнинг таких нейроночек + внешние средства проверки правильности типа того же прувера, могут реально толкнуть вперёд всю эту тему настолько, что свидетелям эйдосов и "превосходства человека над бездушной машиной" может реально поплохеть от возможностей автоматизированного доказательства. Не будем забывать, что по-сути, простой брутфорс обьебал в шахматы Каспарова ещё в 1997 году.
Аноним 25/01/21 Пнд 12:24:19 1920953325
>>1919740

>горький петух со своим форсом ... таких нейроночек
съебите со своими нейтроночками, плиз, все доски уже засрали, чесслово. мы тут о высоком, а они всё о своём.

>Каспарова ещё в 1997
вы приводите Каспарова в качестве примера прувера? иначе зачем?
Аноним 27/01/21 Срд 11:55:01 1923052326
>>1920953
> мы тут о высоком,
А это и есть высокое, выше некуда.
> вы приводите Каспарова в качестве примера прувера? иначе зачем?
Куда тебе до высокого, если ты даже такой элементарный пример понять не в состоянии.
Аноним 28/01/21 Чтв 12:09:56 1924179327
>>1923052
>А это и есть высокое
>Куда тебе до высокого
ваш "ИИ" пузырь раздули инвесторы всего несколько лет назад.
еще через пару лет инвесторы выйдут со своими деньгами (иначе зачем они заходили), а бывшие МЛ-стартаперы побегут за новым хайпом хвалить что-то новое "высокое".
Аноним 28/01/21 Чтв 12:10:38 1924180328
>>1924179
анон гарантирует это
Аноним 29/01/21 Птн 11:35:52 1924996329
>>1924179
Да-да, немного потерпеть и прогресс остановится.
Аноним 29/01/21 Птн 18:12:30 1925381330
>>1924996

прогресс не остановить

40 лет назад пруверы работали кое-как и велись исследования
в наши дни пруверы работают кое-как и ведутся исследования
и еще через 40 лет пруверы будут работать кое-как и еще активнее будут вестись исследования

потому что пруверы - это о высоком
это компутер сайенс и рисёрч, а ваши вшивые стартапы
это прогресс
Аноним 29/01/21 Птн 18:27:55 1925393331
>>1925381
> 40 лет назад пруверы работали кое-как и велись исследования
40 лет назад пруверов не было, гейний. Automath не прувер.
Аноним 29/01/21 Птн 18:30:08 1925399332
>>1925393
>Automath
сами себе ответили
Аноним 01/02/21 Пнд 11:38:34 1927671333
>>1905167
>А кто будет сторожить сторожа?
Аноним 04/02/21 Чтв 22:14:36 1930844334
>>1927671
можно ли верифицировать Coq в Coq? или хотя бы в агде
Аноним 04/02/21 Чтв 22:27:28 1930846335
>>1747168
> Кстати, чому пруверам на учат в школе?
А какое-то математическое ПО вообще используют в школе? Может в вузе?
Аноним 05/02/21 Птн 10:26:47 1931056336
>>1930846
В вузах разве что Matlab/Mathcad, но это всё не то.
Аноним 05/02/21 Птн 22:40:44 1931747337
>>1930846
>математическое ПО
Эксель
Аноним 06/02/21 Суб 06:58:16 1931952338
>>1931747
Бля, нам один препод в течение нескольких курсов давал один и тот же курсач, где надо было в ебучем экселе построить модель со сложной статистикой, и мы там юзали огромные формулы со всякими ДВССЫЛ и СЦЕПИТЬ, графики, сводные таблицы, фильтры, сортироввки, охуеть вообще.
Аноним 07/02/21 Вск 11:26:54 1932988339
>>1512737
разъясните за незаконность, плз
Аноним 07/02/21 Вск 16:29:56 1933349340
>>1932988
Не стоит вскрывать эту тему.txt
Аноним 07/02/21 Вск 19:13:54 1933537341
>>1933349

только самое веселое началось по телевизору, как сразу "детям пора спать".

где вы видели незаконный прувер?

это вам не статические анализаторы или инструменты фаззинга, тут все тихо и академично.

на Ada+Spark летают ракеты, но это никого не интересует, это и так все знают.
Аноним 07/02/21 Вск 19:18:38 1933549342
>>1933349
Написал hello world и калькулятор, — вот и молодец. На этом стоп. Не стоит вскрывать эти конпеляторы и гитхабы. Это тебе не колидоры вычистлительных центров НАСА, даже не датацентры ГУГОЛ, не уютненькие офисы ФЕЙСБУКА. В сферу IT лучше не лезть. Серьезно, любой из вас будет жалеть. Лучше закройте Хабрахабр и забудьте, что тут писалось. Это все вранье, чтобы привлечь как можно больше новых макак на рабочие места и создать демпинг зарплат. Я вполне понимаю, что данным сообщением вызову дополнительный интерес у воротил из Cisco, SAP и IBM, но хочу сразу предостеречь пытливых — стоп. Зарплаты у IT-шников очень унылые. Остальным их просто не дают.
Аноним 08/02/21 Пнд 07:13:36 1933848343
>>1512723
>>1512674 (OP)

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

>ненужности математики

Ахаха. А математике твои пруверы нахер не нужны.
И что теперь?

Даже тред в /pr запилили, а не в /math, наверное, потому что там уже есть загон для подобных шизиков в оснований-тредах.
Аноним 08/02/21 Пнд 07:25:01 1933854344
Аноним 08/02/21 Пнд 11:22:46 1934019345
>>1933537
На сильную систему типов почему-то надо получать лицензию, на слабую нет.
Аноним 08/02/21 Пнд 15:34:15 1934311346
>>1934019
кто выдает лицензию?
Государственная комиссия по радиочастотам?

на куртяник Agda|Coq уже есть лицензия?
Аноним 08/02/21 Пнд 15:42:55 1934320347
>>1885703
вы же в курсе, что Thierry Coquand [Coq] & Catarina Coquand [Agda-1] не случайно имеют одну фамилию
Аноним 12/02/21 Птн 15:34:44 1938627348
censorphotoshop[...].jpg 35Кб, 526x526
526x526
где тот человек, который тут писал про собственный язык "говяжий"? у него что-то получилось? превзошел NuRPL и Twelf?
Аноним 14/02/21 Вск 18:42:18 1940878349
После получения базового теоретико-категорного mind-set от вебмакакинга тошнит, аж трясет, блядь. Интересно, что дальше будет.
Аноним 15/02/21 Пнд 11:52:15 1941588350
>>1940878
В конце ты сдохнешь
Аноним 15/02/21 Пнд 14:50:18 1941873351
>>1940878
Да ты просто в интерфейсах не разбирается, чтобы для них категории применить.
Аноним 16/02/21 Втр 01:52:12 1942697352
image.png 155Кб, 1570x665
1570x665
Аноним 21/02/21 Вск 20:22:29 1948657353
Требую scratch для пруверов!
Аноним 22/02/21 Пнд 21:24:31 1949419354
>>1948657
Куда тебе в пруверы, если ты писать не умеешь
Аноним 23/02/21 Втр 00:00:05 1949483355
Парни, а о чем тред?
я даже это не осилил
Аноним 23/02/21 Втр 01:34:48 1949523356
image.png 355Кб, 791x960
791x960
>>1949483
Вот есть типа книги по математики там. И там теоремы всякие. Они доказываются как на картинке и их никто не проверяет, просто люди от балды лепят себе звания академиков там всяких.

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

А доказательство это типа про типизацию.
Аноним 23/02/21 Втр 22:54:40 1950273357
>>1949483
тред об том, как сделать, чтобы ракеты не падали мимо цели, и чтобы рентгеновский аппарат не просверлил поциента лучом внезано из-за опечатки васяна-прогламмера. впрочем, БОИНГУ даже это не помогло.
Аноним 23/02/21 Втр 22:59:21 1950275358
>>1950273
впрочем, не программистам верифицировать программы, этим должны заниматься профессиональные логики и математики.
Аноним 23/02/21 Втр 22:59:56 1950276359
>>1950275
имею ввиду верифицировать подобного рода софт, который относится к ракетостроению, например.
Аноним 23/02/21 Втр 23:12:35 1950281360
>>1950273
> даже это не помогло
Вывод: неработающая хуйня без задач.
/thread
Аноним 23/02/21 Втр 23:23:14 1950286361
>>1949523
>>1950273
Т.е автоматическая проверка софта на соответствие нормам и необходимым критериям?
Аноним 24/02/21 Срд 04:18:08 1950376362
>>1938627
Ну он понял, что роботы захватят мир и решил им не помогать. Забросил в 2к17 судя по гитхабу
Аноним 24/02/21 Срд 04:22:17 1950380363
>>1950286
Софт пишешь руками
Критерии пишешь руками
Пруфы, что софт соответствует критериям пишешь руками

Прувер проверят внезапнокорректность пруфа.
Аноним 24/02/21 Срд 04:29:52 1950385364
Верифицировать недоеденное дедовское говно типа С готовый софт - дело изначально не очень. Compcert и VST для кока и вот это все ящитаю путь в никуда. Нужно сразу писать корректный код, именно для этого делается Идрис, особенно Идрис 2. Сразу написал что тебе нужно и сконпелял нужным кодгеном в нужный формат. Брэди пока единственный шарит куда нужно воевать в плане средств написания корректного софта, остальное это полумеры и костыли. Алсо, он очень молодец что дропнул хачкелепомойку, теперь Идрис 2 ставится одной командой в бубунте с помощью стандартного snapcraft'а. Алсо, не стесняется признавать своих ошибок, так и сказал, что первый Идрис нормально не допилить, а QTT лучше чем его подход, на тему которого он написал диссертацию.
Аноним 24/02/21 Срд 04:54:28 1950387365
>>1950385
>QTT
>диссертацию
Хватит пугать.
Аноним 24/02/21 Срд 14:57:46 1950569366
>>1949483
>>1949523
>>1950273
Тред о том, что шизики-конструктивисты всё ещё пытаются сделать вид, что они могут в математику, и что они вообще нужны.

Их периодически пытаются пидорнуть из /math, вот они в /pr и перекатываются.
Аноним 24/02/21 Срд 16:39:06 1950659367
>>1950569
ЯМы хотим пруфать код. Гомологии и пучки тут никому не интересны
Аноним 24/02/21 Срд 18:04:45 1950739368
>>1950659
>ЯМы ...
... Алексей Навальный!
Свободу политзаключенным!
Россия будет счастливой!
Аноним 24/02/21 Срд 22:07:44 1950949369
разве это не замечательно, когда собравшиеся доны после более года куртуазных обсуждений где-то в районе 365-го сообщения начинают ВНЕЗАПНО выяснять, о чем же был, собственно, этот тред.
Аноним 24/02/21 Срд 23:00:14 1950969370
>>1950659
код пускай пруфает солвер (осталось его написать).
человек нужен только, чтобы задавать вопросы сочинять спецификации и архитектуру.

"компьютер бесполезен - он может только давать ответы" (с) Пикассо
Аноним 24/02/21 Срд 23:49:57 1951004371
>>1950969
>осталось его написать
Бля хуйня какая. Что же сразу не сказали, ща напишу.
Аноним 24/02/21 Срд 23:54:43 1951007372
>>1950949
Хлебаем борщи уже больше двух лет, а он только опомнился
Аноним 25/02/21 Чтв 05:48:41 1951073373
У меня складывается впечатление, что кроме меня тут с верификацией кода вообще никто не сталкивался. А потом пришел модульный долбаеб без мозгов пучками трясти... Но я всё-таки спалю годноту быдлу, новый 5ый том software foundation https://softwarefoundations.cis.upenn.edu/ полностью посвящен основам этого дела на примере кока и уже упоминавшегося мной VST с написанным для него верифицированным подмножеством С. Я не перестал считать это направление путем в никуда, но как введение в предмет - вполне годно.
Аноним 25/02/21 Чтв 09:10:22 1951108374
>>1951073
>А потом пришел модульный долбаеб без мозгов пучками трясти...
Что ты имеешь против математики?
Аноним 25/02/21 Чтв 12:19:29 1951204375
>>1951108
> Что ты имеешь против математики?
Ничего. Модульный долбаеб != математика.
Аноним 25/02/21 Чтв 16:20:31 1951416376
Аноним 25/02/21 Чтв 19:48:45 1951671377
>>1951073
>с верификацией кода
И что ты такого делал?
Аноним 25/02/21 Чтв 20:03:37 1951681378
>>1951671
верифицировал, что 1+1==2
Аноним 25/02/21 Чтв 20:57:26 1951709379
>>1951681
Читать научись, маня. Там про код написано.
Аноним 25/02/21 Чтв 21:31:27 1951741380
>>1951709
Формально верифицировал, что noop ничего не возвращает и то что функция identity возвращает свой аргумент.
Аноним 26/02/21 Птн 08:27:32 1951945381
>>1951073
>кроме меня тут с верификацией кода вообще никто не сталкивался
Наверное.
>на примере кока и уже упоминавшегося мной VST с написанным для него верифицированным подмножеством С
А что даст полная верификация всего С?
Любая программа на верифицированном С будет верифицированной?
Я не шарю.
>Я не перестал считать это направление путем в никуда, но как введение в предмет - вполне годно.
Почему это путь в никуда?
Аноним 27/02/21 Суб 19:03:04 1953294382
>>1951945
>Почему это путь в никуда?
>А что даст полная верификация всего С?
я не тот анон, но один ваш вопрос отвечает на другой.
Аноним 27/02/21 Суб 20:16:36 1953345383
>>1953294
Не выкайте мне, я с вами на вы не переходил, я не вы, а ты.
Аноним 27/02/21 Суб 21:45:51 1953400384
>>1953294
Спасибо.
Но я так и не понял, это путь в никуда, потому что полная верификация ничего не даст, или полная верификация - это путь в никуда?

>>1953345
Но ведь ты не я. А он отвечал мне.
Но ко мне тоже не надо на "Вы". Это же Двачи, тут принято хуями крыть, а не на "Вы" обращаться.
Аноним 27/02/21 Суб 22:01:00 1953421385
Аноним 28/02/21 Вск 00:11:54 1953505386
>>1951945
> Любая программа на верифицированном С будет верифицированной?
Да. Но его полностью верифицировать невозможно, хотя теми чуваками верифицирована бОльшая часть.
> Почему это путь в никуда?
Потому что С не про верификацию, его создавали без учёта таких возможностей, это уже недавно придумали. Как я говорил выше, правильный путь - изначально верифицированный код. И лучший вариант это написание кода на чем-то одном, а затем его компиляция кодгенами во что угодно, как и работает Идрис 2.
>>1953400
> Но я так и не понял, это путь в никуда, потому что полная верификация ничего не даст, или полная верификация - это путь в никуда?
Полная верификация С невозможна, что доказал Аппель сотоварищи. А та часть, которая таки верифицируема, ее намного проще генерировать кодгеном в идрисе.
Аноним 28/02/21 Вск 00:46:24 1953529387
>>1953505
> > Любая программа на верифицированном С будет верифицированной?
> Да.
Для того, чтобы программа на С была верифицирована, ей же нужна спецификация, не? Т.е. любую программу на С надо или переписывать, или дописывать. Без спек, можно доказать отсутствие UB, "корректность" работы с памятью и проч.
Что я не так понимаю?
мимо пятую книгу не читал
Аноним 28/02/21 Вск 00:52:14 1953531388
Вот представьте себе - верифицировали тот же Идрис на Идрисе, к примеру. Никаких сомнений уже нету. А потом вдруг выясняется, что система типов такая, что можно доказать Bottom. BINGO! Потом ее пофиксили, а через год опять нашли новый Bottom. А через год опять. Bottom - это полная жопа, никто не застрахован.
Аноним 28/02/21 Вск 00:59:23 1953533389
>>1953531
Замечательно же. Язык на котором, чтобы обосраться нужно постараться, лучше чем наоборот.
Аноним 28/02/21 Вск 10:43:15 1953627390
Бамп.
Аноним 01/03/21 Пнд 08:43:44 1954344391
Аноним 01/03/21 Пнд 08:47:46 1954346392
>>1512674 (OP)
Возможно ли теоретически построение верификатора, верифицирующего самого себя?
Или это алгоритмически неразрешимая задача?
Аноним 01/03/21 Пнд 09:18:33 1954358393
>>1954346
Теорема Геделя в помощь.
Аноним 01/03/21 Пнд 09:37:22 1954366394
Аноним 01/03/21 Пнд 10:44:20 1954407395
>>1954346
Как бы можно, но нет уверенности в результатах. Если в верификаторе изначально есть изъян, то собственный код она сверефицирует неправильно.
Аноним 01/03/21 Пнд 11:13:49 1954420396
>>1954344
Это как Бабай.
Слово такое есть, а его самого нет.
"То, чаво не может быть".
Аноним 01/03/21 Пнд 15:55:51 1954714397
Аноним 01/03/21 Пнд 16:05:37 1954722398
>>1954420
А я думал, отсылка к Спанч Бобу.
Аноним 01/03/21 Пнд 16:25:44 1954754399
Аноним 01/03/21 Пнд 20:51:39 1954977400
>>1953531
> А потом вдруг выясняется, что система типов такая, что можно доказать Bottom. BINGO! Потом ее пофиксили, а через год опять нашли новый Bottom. А через год опять. Bottom - это полная жопа, никто не застрахован.
Бред какой-то. Почитай хоть, что это вообще такое. Какой ещё "новый bottom"? То Геделя приплетут, то вообще ШУЕ ППШ какое-то.
Аноним 01/03/21 Пнд 22:59:22 1955086401
>>1954977

Если не понятно, то так и надо говорить.

Достаточно почитать багтрекеры известных пруверов, за которые здесь топят, как вскрываются интереснейшие подробности.
Аноним 01/03/21 Пнд 23:02:35 1955088402
>>1512723
А зачем все это нужно? Какую проблему вы решаете?
Аноним 01/03/21 Пнд 23:33:05 1955109403
>>1955088
лучше Дейсктры никто не объяснит!
Аноним 01/03/21 Пнд 23:47:19 1955121404
>>1955109
сохацкий не палится
Аноним 01/03/21 Пнд 23:49:25 1955122405
>>1955121
от сохацкого слышу
Аноним 02/03/21 Втр 01:29:10 1955165406
>>1955109
Если. Человек не модет объяснить реьегку, чем он занимскется, этот человек ничем не занимается.
Аноним 02/03/21 Втр 07:32:20 1955192407
Аноним 02/03/21 Втр 11:23:38 1955270408
>>1949483
>Парни, а о чем тред?
Обколются своими пруверами, а потом сидят со стеклянным взглядом, исполняя странные пассы руками.
https://www.youtube.com/watch?v=w-HuQun8Cgc
Аноним 02/03/21 Втр 13:49:18 1955395409
Аноним 02/03/21 Втр 14:30:00 1955428410
>>1955395
>Сынок, ты не понял.
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="Ваш+жалкий+практический+земной+мирок+не+нужен"

Человек-мем.
Аноним 02/03/21 Втр 19:28:42 1955682411
>>1955428
и ни слова о контрактном программировании, что характерно
Аноним 10/04/21 Суб 06:17:35 1991606412
Интересный тред. Жаль я не программист.
Аноним 10/04/21 Суб 12:39:35 1991731413
Доказательства это гиблое и не нужное дело, нужно развивать систему тестирования. Тот же Эвклид уже не нужен так как есть аналитическая геометрия, где ничего доказывать не нужно, а просто и понятно работают над векторами.
Аноним 10/04/21 Суб 12:52:01 1991740414
>>1991731
Нормальный учебник по аналитической геометрии начинается с аксиоматики. Но откуда тебе это знать, в твоем заборостроительном вузе.
Аноним 10/04/21 Суб 13:03:53 1991745415
>>1991740
Обычно как раз в конце в силу традиции дедов.
Аноним 10/04/21 Суб 14:26:58 1991814416
Свободный инструментарий для доказательства теорем Coq рассматривает возможность смены названия. Причина: для англофонов слова "coq" и "cock" (сленговое название мужского полового органа) звучат похоже, и некоторые пользователи-женщины, сталкивались с двусмысленными шутками при использовании названия в устной речи. Само же название языка Coq произошло от фамилии одного из разработчиков, Thierry Coquand. Сходство звучания Coq (фран. петух) и Cock (англ. петух) уже обыгрывалось в проекте: язык, используемый для описания конструкций, называется Gallina (лат. курица).
Аноним 10/04/21 Суб 14:54:49 1991865417
Аноним 11/04/21 Вск 13:16:04 1992621418
>>1991814
Какая разница, как называть, главное чтобы работало. А название пусть хоть крокодилзалупасыр будет.
Аноним 11/04/21 Вск 16:58:08 1992784419
>>1991814
>пользователи-женщины,
А coqомрази могут и потерпеть
Аноним 11/04/21 Вск 17:45:40 1992821420
>>1992621
Какая разница как назвать нигеров, главное чтобы работали))0
Аноним 17/04/21 Суб 08:34:55 1998775421
идрис говно и моча
Аноним 17/04/21 Суб 19:21:05 1999411422
>>1998775
Да, но почему ты это написал?
Аноним 17/04/21 Суб 21:12:07 1999556423
>>1998775
Первая или вторая версия?
Аноним 22/04/21 Чтв 21:50:50 2004941424
>>1999556
вторая хуже первой
Аноним 22/04/21 Чтв 21:51:15 2004942425
>>1999411
могу себе позволить
Аноним 24/04/21 Суб 02:07:23 2006397426
Аноним 26/04/21 Пнд 19:58:52 2009486427
Аноним 01/05/21 Суб 06:40:28 2014660428
Идрис это больше про корректный код, а не про прувер. Современный код настолько примитивен, что даже парадокс Жирара в системе типов не мешает. Алсо допилят же, там до первого релиза ещё как до Луны пешком. Огромный плюс в идрисе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.
Автозаполнение дыр теперь работает на уровне всего кода.
Аноним 01/05/21 Суб 08:00:29 2014678429
Добавлю.
>>2014660
> Holes are global to a source file, rather than local to a definition, meaning that some holes can be left in function types to be inferred by the type checker.
То есть, при правильной организации кода, тайпчекер сам почти все напишет за тебя. Ставишь задачу, импортируешь нужные модули, расставляешь дыры (что нужно дописать) и тайпчекер сам их заполняет. Потом просто кодгеном получаешь исходник на нужном яп, причем, это гарантированно корректный код. Type-driving development это реально будущее программирования. Лямбды только сейчас завозят в мейнстримные параши, лет через 30 то что уже сейчас может Идрис2, завезут в мейнстрим.
Настройки X
Ответить в тред X
15000
Макс объем: 40Mб, макс кол-во файлов: 4
Кликни/брось файл/ctrl-v
Стикеры X
Избранное / Топ тредов