DS
Чуть по другому выражена и всё
Size: a a a
2021 February 01
ΑZ
Я — тупой и не умею в математику.
Научись, она сложнее сериальчиков но понять можно любому
EG
По ощущению
ΑZ
Да там нет ничего, кроме мозголюбия. Любой исходник на идрисе читается как латехный пейпер.
С агдой не перепутал?
DS
Да там нет ничего, кроме мозголюбия. Любой исходник на идрисе читается как латехный пейпер.
Потому что ты смотришь на тех, кто юзает зав типы непосредственно для доказательств корректности.
r
Научись, она сложнее сериальчиков но понять можно любому
citation needed
EG
Потому что ты смотришь на тех, кто юзает зав типы непосредственно для доказательств корректности.
Типы вообще нужны для доказательств корректности
SP
Ну, да, можно построить красивую систему типов на основе красивой математики. А можно использовать кривой, не идеальный костыль, который можно будет понять без красивой математики.
царь - 1. запарта - 0
DS
Типы вообще нужны для доказательств корректности
Имеется в виду - для доказательств полного соответствия данного алгоритма своей полной спецификации.
DS
А это везде - головная боль и проблема
DS
Если юзать зав типы просто для увеличения выразительности, то проблем особо не будет.
EG
царь - 1. запарта - 0
Я не умею парсить царя
И ещё больше я не умею парсить двадцатые плюсы с бустом
И ещё больше я не умею парсить двадцатые плюсы с бустом
EG
Я понимаю, что он мб что-то интересное сказать хочет, но прочитать не могу
DS
Как пример - та же скала обладает зависимыми типами внутри (в некотором ограниченном качестве, но всё равно), при этом никто на ней пруфы, очевидно, не пишет и уровень мозголомства там не больше чем в каком-нибудь расте.
(Где тоже повсюду легкий тайплевел, хаки и т.п.)
(Где тоже повсюду легкий тайплевел, хаки и т.п.)
EG
Как пример - та же скала обладает зависимыми типами внутри (в некотором ограниченном качестве, но всё равно), при этом никто на ней пруфы, очевидно, не пишет и уровень мозголомства там не больше чем в каком-нибудь расте.
(Где тоже повсюду легкий тайплевел, хаки и т.п.)
(Где тоже повсюду легкий тайплевел, хаки и т.п.)
В скале уровень мозголомства на порядок больше, чем в расте, потому что имплиситы не позволяют рассуждать локально про что-либо
DS
В скале уровень мозголомства на порядок больше, чем в расте, потому что имплиситы не позволяют рассуждать локально про что-либо
Смотря как их использовать.
DS
Если их использовать, как это делают в реальной жизни, то сравнимо с тем же растом вполне себе
DS
Если их использовать unironically для пробрасываний каких-то значений, а не для "тайпклассов" - то да, конечно будет ебанавтика.
DS
Но так в 2021м никто не делает
A
ну конечно, и посмотри на волшебный результат
В Средневековье с этим проблем не было.