AG
в конструктивном стиле доказательства превращаются в (мета)программы
Size: a a a
2021 March 10
AG
вот смотри, я тут надоказывал чего-то, а теперь скажи мне что это за утверждение, чудо-машина
да, именно поэтому тайп инференс довольно сомнительная идея с логической тз
AG
макбрайд неоднократно высказывался уже
AT
нужен теперь макгрум — дополнить макбрайда
AG
это всё связано с давешним димсоловским вопросом про использование символьной алгебры, т.е. штук типа mathematica
AG
https://t.me/scala_ponv/1260300 вот тут был тред, только димсол конечно как водится свои реплики потёр
AG
конструктивный аналог доказательства разрешимости для какой-то алгебраической теории это и есть алгоритм символьной алгебры
AG
или не выдаст ничего
контрпруф выдаст же
AG
если повезет даже реифицированный, как я показывал на секвенции-семинаре для тайпчекинга лямбды :)
AG
т.е. конкретный контрпример в индуктивном виде
AG
если ничего не выдаст, это semidecidability :)
AT
если ничего не выдаст, это semidecidability :)
в том контексте показалось, что ещё в общем случае было)
R
что то понял, спасибо
R
а то не вежливо молчать наверное
AG
"на Плутон" надо было еще :)
AG
норм: претопосы и рандомное тестирование
в принципе по большому счёту он изобрел что-то довольно близкое к ссрефлекту идеологически, нет?
AT
в принципе по большому счёту он изобрел что-то довольно близкое к ссрефлекту идеологически, нет?
я пока ещё не смотрел — сижу подновляю лекцию на завтра
AG
надо бы тоже поработать
w
надо бы тоже поработать
Эх, сча бы поработать