История изменений
Исправление crutch_master, (текущая версия) :
Разные подходы и системы типов - это попытки придумать всё более мощный язык описания этой неправильности. Начиная от простейшей типизации в Си и заканчивая всякими системами зависимых типов.
Это метаязык, язык над языком, который призван в формальной логике задавать соотношения предметной области так, чтобы машина была способна проверить рассуждения автора и найти в них ошибку.
Это всё хорошо. И было бы вообще отлично, если имело какое-то отношение к мейнстримовым ст недоязычкам.
Вот на динамике метаязык можно построить очень легко. В ст язычке - нет. Что автор выдавил из себя, то и жри.
Исходная версия crutch_master, :
Разные подходы и системы типов - это попытки придумать всё более мощный язык описания этой неправильности. Начиная от простейшей типизации в Си и заканчивая всякими системами зависимых типов.
Это метаязык, язык над языком, который призван в формальной логике задавать соотношения предметной области так, чтобы машина была способна проверить рассуждения автора и найти в них ошибку.
Это всё хорошо. И было бы вообще отлично, если имело какое-то отношение к мейнстримовым ст недоязычкам.
Вот на динамике метаязык можно построить очень легко. В ст язчке - нет. Что автор выдавил из себя, то и жри.