AT
гг как раз только что обсуждали тлю с алексом
прошлись по лэмпорту за то, что он типы не любит?
Size: a a a
2021 February 15
AG
ага :) чувствуется это его любимая байка
AG
ну он в целом невысокого мнения о модел чекерах
AG
типа без хорошей фундаментальной теории это всё деньги на ветер
AG
задумался кстати насколько полезно может быть файнал тэглесс представление для денотационной семантики того же фцсля
AG
по идее в расширяемости можно выиграть если часто менять
AT
типа без хорошей фундаментальной теории это всё деньги на ветер
в пл сообществе они пока не сильно прижились, а в системах уже почти стандарт дефакто
AG
в пл их тоже вовсю пихают в тайпчекеры, в granule например
AG
но типа пойнт Алекса в том что там слишком много инвестируют сил в процедуры разрешимости адхочные
AG
и когда выходит более изящная теория типа той же сепарационки, оно все моментально устаревает
AT
хех, ну это похоже на иногда встречающуюся претензию к авторам теорий: чтой-то они не делают свою теория в максимально общей форме с первого раза?
λ
решил посмотреть дегуза про смерть тф
λ
а он там ковидом всех заражает
V
зассал забыть трэвиса не про жизнь ЗИО
она тут никого не исцеляет от вида
она тут никого не исцеляет от вида
V
@odomontois правильно?
AT
в пл их тоже вовсю пихают в тайпчекеры, в granule например
посмотрел абстракт гранулы от айсиэфпи 2019, но там они про модел чекинг не говорят
как они его применяют?
как они его применяют?
AT
> We provide a bidirectional type checking algorithm (ğ5), at the heart of our implementation,
which exploits an SMT solver to discharge theorems over the indices of graded modalities.
а ну это я бы не назвал классическим state-exploration модел-чекингом
which exploits an SMT solver to discharge theorems over the indices of graded modalities.
а ну это я бы не назвал классическим state-exploration модел-чекингом
AG
солвер да, не чекер
AG
вся тема с рафинадом по моему на солверах держится
AG
про модел-чекинг я всё хочу покурить папирусы миллера