What about the venerable "match types"? 😂

А вот это как раз "навертели", это механизм, он в формальной модели DOT ещё не формализован и в предыдущих версиях компилятора порождал unsound. Там вроде дырки позатыкали, но пока непонятно

Но опять же он выразительные свойства не сильно расширяет.
Всё, что выразимо через match types, выразимо через GADT

только с боксингом

Вот это надо вынести в Preface тоже

Видимо, это и есть корень всех проблем в программировании... 😔

четверг 10 февраля 2022 г. с 11:00 до 12:30 по московскому времени
Онтологический подход к дедуктивной верификации императивных программ
Аннотация: В докладе будет представлен онтологический подход к дедуктивной верификации императивных программ. Основой подхода являются новый вид систем переходов - атрибутные системы, язык спецификации атрибутных систем ASL и новые виды семантик императивных языков программирования - онтологическая, онтологическая операционная и онтологическая логическая. Подход будет проиллюстрирован на модельном императивном языке.
https://persons.iis.nsk.su/ru/ruSTEP