Исправление quasimoto, (текущая версия) :
то, что ты там быдлокодишь
А какая _теория_ нужна для быдлокодинга? По-моему, никакой :) Простейшая линейная алгебра, реляционная алгебра или численные / вычислительные разделы математики понятно как применяются, но это всё отдельные области. А если задаться вопросом какая математическая метатеория годится для изучения программирования в целом, то какой напрашивается ответ? И какие вообще есть варианты? Могут быть разные ответы, ТК отличается тем, что в ней можно смоделировать эти разные варианты и посмотреть как они связаны.
Есть прямая связь типизированного лямбда исчисления и CCC, зависимых типов и LCCC, существуют модели пи-исчисления (которое само по себе шире лямбда-исчисления).
Но сугубо практических применений я не знаю - только бэкграунд, сопутствующая терминология и инструмент для CS теоретизирований (которыми непосредственные инженеры не занимаются). Но, например, если какой-то теоретик докажет что некая метатеория всячески правильна и непротиворечива, то основанный на этой метатеории ЯП тоже будет таким (либо его подмножество, если его чётко выделить), при этом пишущие реализацию люди могут пользоваться той терминологией которую предпочитают, например, категорной.
Исходная версия quasimoto, :
то, что ты там быдлокодишь
А какая _теория_ нужна для быдлокодинга? По-моему, никакой :) Простейшая линейная алгебра, реляционная алгебра или численные / вычислительные разделы математики понятно как применяются, но это всё отдельные области. А если задаться вопросом какая математическая метатеория годится для изучения программирования в целом, то какой напрашивается ответ? И какие вообще есть варианты? Могут быть разные ответы, ТК отличается тем, что в ней можно смоделировать эти разные варианты и посмотреть как они связаны.
Есть прямая связь типизированного лямбда исчисления и CCC, зависимых типов и LCCC, существуют модели пи-исчисления (которое само по себе шире лямбда-исчисления).
Но сугубо практических применений я не знаю - только бэкграунд, сопутствующая терминология и инструмент для CS теоретизирований (которым непосредственные инженеры не занимаются). Но, например, если какой-то теоретик докажет что некая метатеория всячески правильна и непротиворечива, то основанных на этой метатеории ЯП тоже будет таким (либо его подмножество, если его чётко выделить), при этом пишущие реализацию люди могут пользоваться той терминологией которую предпочитают, например, категорной.