VD
Тут ещё довольно понятно всё
Ну если вчитываться аккуратно, то может и да.
Size: a a a
2020 October 23
VD
Надо было не прогуливать матаний, сейчас бы может умным был.
DF
когда уже на ghc rts на русте перепишут
Когда pressure to publish перестанет на клапан давить
AG
это спецификация на сепарационной логике разворота связного списка через pointer swinging
R
А тебе в ответ "всё фигня, переделывай", а потом еще и на личности переходят.
На позицию джуниор Web аппликатор
AG
ключевая идея в том что можно привязать определение "списка как пачки ячеек сцепленных указателями" к определению "списка как индуктивной структуры"
AG
про второе доказывать сильно проще
AG
в этом в общем то и был изначальный смысл фп - это язык спецификаций, про который удобно что-то логически доказывать
AG
только потом решили что мол давайте этот язык напрямую на железе запускать
DF
Ого интересно
AG
ну ML появился как язык тактик для семейства LCF пруверов
AG
под фп я тут понимаю клапауциевщину с твердым ядром конечно
DF
А пруверы сами же на железе бежали
DF
Но были видимо на пл/1 написаны
AG
пруверам не надо было ничего рантаймного производить, достаточно чтобы прочекалось
DF
Понятно
AG
идея с экстракцией кода из доказательств и пруф-релевантностью тоже позднейшая
AG
если вдаваться в подробности, то это по сути разница между классической и конструктивной логикой
AG
математики и логики традиционно всегда работали с классическими доказательствами, потому что они удобнее и привычнее
DF
Классическая для рантайма? )