DS
Size: a a a
2020 July 05
ЕГ
Каким путем мне тогда изучить теорию типизации?
Зайди на 2ality там у чувака есть книжка с ТС попробуй там, правда она неполная так как надо задонатить, но так чисто думаю лишним не будет
DS
Зайди на 2ality там у чувака есть книжка с ТС попробуй там, правда она неполная так как надо задонатить, но так чисто думаю лишним не будет
Эта?
ЕГ
Ага
DS
Ага
Спс
🚀🚀
Aleksandr Osipov
Agda, Idris :)
рекомендую попробовать самому, крайне отрезвляющий экспириенс https://t.me/effector_ru/135048
🚀🚀
у соседа за забором всегда трава зеленее
AO
рекомендую попробовать самому, крайне отрезвляющий экспириенс https://t.me/effector_ru/135048
Так смайл не зря там был, когда-то я угорал сильно по фп, начиналось все безобидно с хаскелла (у нас коллеги возились чуток с ним, когда что-то делали с seL4) и собственно там я увидел формальное доказательство корректности реализации со спекой L4, само док-во было на Isabelle HOL написано, я тогда нихрена не понял, но начал копать глубже
AO
Потом правда пришло понимание (читай что я неосилил) что в прикладных задачах все это малоприменимо
FB
Лол
🦜
Думаю, здесь это не нужно
🦜
Выглядит как сокрытие пиара
FB
Да пжлста
DS
Aleksandr Osipov
Так смайл не зря там был, когда-то я угорал сильно по фп, начиналось все безобидно с хаскелла (у нас коллеги возились чуток с ним, когда что-то делали с seL4) и собственно там я увидел формальное доказательство корректности реализации со спекой L4, само док-во было на Isabelle HOL написано, я тогда нихрена не понял, но начал копать глубже
Скока меня можно разводить?:)
Я же бедный формашлеп...
Я же бедный формашлеп...
AO
Скока меня можно разводить?:)
Я же бедный формашлеп...
Я же бедный формашлеп...
Кстати на счет формошлепства, сначала я как во фронт пришел меня прямо задевало сильно
AO
Со временем поев всякого на проектах состоящих на 90 процетов из форм, понял что задача то не такая тривиальная, и просто перестал обращать внимание на такие насмешки
DS
Aleksandr Osipov
Со временем поев всякого на проектах состоящих на 90 процетов из форм, понял что задача то не такая тривиальная, и просто перестал обращать внимание на такие насмешки
Можно принять как комплимент в свою сторону?))
D
Почему из раза в раз приходится в 10000 раз писать очередную форму состоящую всё из того же и делающую всё то же, но в этот раз на другом SSM и в других папочках? Почему круды ещё не генерируются под любую задачу на свете сами?
AO
Можно принять как комплимент в свою сторону?))
Ну если так хочешь:) я вообще про то что не стоит так уничижительно о своей деятельности говорить
AO
Почему из раза в раз приходится в 10000 раз писать очередную форму состоящую всё из того же и делающую всё то же, но в этот раз на другом SSM и в других папочках? Почему круды ещё не генерируются под любую задачу на свете сами?
У меня круды как раз генерируются:)