SB
тут не знаешь как Эрланг осилить! а вы говорите Idris
Size: a a a
2020 March 27
SB
я как-то на TLA+ замахнулся
SB
даже немного асилил
DS
Надо почитать про это все. Для меня пока темный лес.
Тут на этой идее оно основано: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
SB
и потом понял, что у меня ни одной задачи, где его можно применить
SN
тут не знаешь как Эрланг осилить! а вы говорите Idris
эрланг крайне прост, там просто практика нужна. проще, чем питон
DS
Idris книжку имеет офигенну, по Agda есть что-то похожее?
Есть не настолько офигенная книжка. Но агда при этом заточена под доказательство теорем прежде всего
SN
Есть не настолько офигенная книжка. Но агда при этом заточена под доказательство теорем прежде всего
ну хоть какая-то? я Programming in Scala прочитал от начала до конца последовательно, ничего, не умер
SB
эрланг крайне прост, там просто практика нужна. проще, чем питон
ну нет, если ты пытаешься вникнуть в то как оно под капотом работает и как вообще у них все это получилось.
SN
ну нет, если ты пытаешься вникнуть в то как оно под капотом работает и как вообще у них все это получилось.
для запиливания проекта на эрланге это лишнее, ты и про эфшарп такого не знаешь. но пишешь как-то
SB
Тут на этой идее оно основано: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
но основную суть этого изоморфизма я вроде бы понимаю, все хотел про это тоже что-то узнать и все не было повода. вот теперь есть.
DS
ну хоть какая-то? я Programming in Scala прочитал от начала до конца последовательно, ничего, не умер
Хоть какая-то есть, небольшой курс в инете.
SB
я нынче знакомлюсь с https://ru.wikipedia.org/wiki/%D0%90%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC_%D0%9F%D0%B0%D0%BA%D1%81%D0%BE%D1%81. ну и вообще, заполняю дыры в моем понимании основных проблем, решений и принципиально неразрешимых задач в распределенных системах. после всяких там теоркатов читается очень по-другому.
VP
SB
для запиливания проекта на эрланге это лишнее, ты и про эфшарп такого не знаешь. но пишешь как-то
та меня больше идеи интересуют и архитектурные принципы. вот кто-кто, а Джо Армстронг и как там его товарища звали родили совершенно уникальное явление на небосклоне программирования.
VS
Под вечер пятницы тут из конторы новости подваливают из-за пандемии - сначала сказали что объявляют банкротство по багам, т.е. 1.5К открытых багов объявляются пофикшенными, а потом сказали что нужно пояса затянуть и зп урезают всем, и добавили что по сравнению с остальными конторами это еще мелочи.
AH
Под вечер пятницы тут из конторы новости подваливают из-за пандемии - сначала сказали что объявляют банкротство по багам, т.е. 1.5К открытых багов объявляются пофикшенными, а потом сказали что нужно пояса затянуть и зп урезают всем, и добавили что по сравнению с остальными конторами это еще мелочи.
Щтоблят5
AH
Вали оттуда нахуй)))
Д
Под вечер пятницы тут из конторы новости подваливают из-за пандемии - сначала сказали что объявляют банкротство по багам, т.е. 1.5К открытых багов объявляются пофикшенными, а потом сказали что нужно пояса затянуть и зп урезают всем, и добавили что по сравнению с остальными конторами это еще мелочи.
Яннп