AG
не, у нас фреймворк для доказательств
Size: a a a
2021 January 11
AG
стм это алгоритм который можно доказать
Oℕ
типа если зохочешь написать СТМ
Oℕ
сможешь полуавтоматически доказать это
Oℕ
понятно да
LO
как всегда у академиков ничего полезного для оперденей
AG
ну там упор не на автоматику как раз
Oℕ
эх
AG
наша логика тип выделяется от всех остальных упором на алгебраичность
Oℕ
наша логика тип выделяется от всех остальных упором на алгебраичность
AG
у нас по сути нет какой то промежуточного логического слоя, а мы сразу проваливаемся в моноиды и манипуляции ими
AG
то есть вот этих всех * и -*
AG
но это нам дает возможность строить околотеоркатовские штуки с морфизмами моноидов
R
электромагнитной радиации в диапазоне 100-300 нм?
Надо ждать новостей.
AG
и соответственно возможностью склеивать с их помощью более сложные пруфы из более простых
LO
когда я уже смогу доказывать опердени?!
AG
там конечно не так всё гладко но кое-какая композициональность на минималках вырисовывается
AG
когда я уже смогу доказывать опердени?!
если у тебя много локфри алгоритмов в оперденях то уже сейчас :)
LO
локфри это для задротов на сиплюсплюс
AG
в нашем случае скорее на жабе, у нас нет (пока) инструментов для работы с рекламацией и слабой памятью