История изменений

Гарантированное завершение компилятора, в его теоретическом понимании, мне неинтересно совершенно.

Да и насрать? Ты явно не шаришь в теме, поэтому твои интересы здесь не играют никакой роли. Как я уже пояснил: очень многие проблемы сводятся к проблеме останова, поэтому её довольно легко и приятно использовать в доказательствах.

Вообще я считаю, что всякие алгоритмические теоретизирования, особенно из середины прошлого века, когда нормальных компов не существовало, на текущий момент для практики бесполезны и не надо их за пределы изысканий теоретиков вытаскивать.

А это не из середины прошлого века. Всякие теории типов Мартина-Лёфа начали появляться в 70х-80х, а в коде их запилили и того позже – в 90х. Для сишника типа тебя это прямо свежачок!

Вообще, между теорией и реализациями в более-менее пригодных для использования инструментах проходит в среднем лет 20. Линейные типы, например, были придуманы как раз в 90х, но реализация в виде Idris и более известного Rust появилась только лет 10 назад. Ждём когда в язычках появятся штуки из HoTT (Гомотопическая Теория Типов).

Гарантированное завершение компилятора, в его теоретическом понимании, мне неинтересно совершенно.

Да и насрать? Ты явно не шаришь в теме, поэтому твои интересы здесь не играют никакой роли. Как я уже пояснил: очень многие проблемы сводятся к проблеме останова, поэтому её довольно легко и приятно использовать в доказательствах.

Вообще я считаю, что всякие алгоритмические теоретизирования, особенно из середины прошлого века, когда нормальных компов не существовало, на текущий момент для практики бесполезны и не надо их за пределы изысканий теоретиков вытаскивать.

А это не из середины прошлого века. Всякие теории типов Мартина-Лёфа начали появляться в 70х-80х, а в коде их запилили и того позже – в 90х. Для сишника типа тебя это прямо свежачок!