...В СССР святой Андрей Николаевич Колмогоров ещё в 1932-м предложил интерпретацию интуиционистской логики, что предвосхитило например изоморфизм Карри-Ховарда (связь между типами и логическими доказательствами). Вообще конструктивная логика была в СССР невероятно сильна, да и теория категорий на высочайшем уровне (школы Гельфанда, Шафаревича, Манина...), только развивалась в основном в контексте топологии.

Андрей Ершов (Новосибирская АН) считался тогда одним из главных теоретиков программирования (смешанные вычисления, частичное вычисление программ...). Но ключевой личностью именно в теме computer science был пожалуй Виктор Глушков (Киевский институт кибернетики). Он работал над теорией автоматов и алгебраическими методами в программировании (программы описывались через алгебраические соотношения, а не через типы и функции), развивал концепцию микропрограммной алгебры... Базовой моделью он выбрал автомат (множество состояний + функция переходов), с алгебраическими операциями над преобразованиями состояний.

Почему так? Советская алгебраическая школа (Мальцев, Курош) считалась сильнейшей в мире, и естественно, что программирование осмыслялось через алгебру, логику и теорию автоматов, а не через теории категорий и типов, которые считались во многом абстрактной чепухой, потому что в СССР был принципиально сделан мощный акцент на тотальную пропаганду прикладной инженерии (чтобы мыслителей-гуманитариев было поменьше, одобряем:).

Информатика развивалась под эгидой кибернетики, которая в советском понимании была про управление, системы, автоматы. Нужно было проектировать ЭВМ, а теория автоматов напрямую описывает железо (конечные автоматы, микропрограммы, схемы), и лямбда-исчисление для этого нафиг не нужно. Между советской категорной математикой и советской информатикой не было вообще никакого моста. Была выбрана алгебра вместо логики, автоматы вместо функций, управление вместо абстракций... Но без лямбда-исчисления нет и не может быть естественного моста между математикой и программированием.

Советская информатика была ориентирована на оборонные и промышленные задачи. Государственный заказ требовал решения конкретных задач: расчёт траекторий ракет, ядерные симуляции, АСУ для плановой экономики. Для этого нужны были только Фортран и Алгол. И хотя велись например фундаментальные исследования в алгебраической семантике (советская математическая школа была топом по работам в алгебраической логике, теории моделей), области чистой теории типов казались чиновникам от науки абстрактной игрой ума, не дающей немедленного экономического или военного эффекта...

Тем временем в Европе (и немножечко в США) начали применять категорную логику к лямбда-исчислению (Ламбек), затем Дана Скотт создал денотационную семантику, связав домены с теоркатом, и уже на основе подобных работ Вадлер и Милнер перенесли это в языки программирования.
И хотя в СССР были мощнейшие математические школы, тот мост, который на Западе соединил категории с типами и полиморфизмом, так и не был построен. И это, пожалуй, совсем грустная история: инструменты были, знания были, люди были -- но они никогда не встретились....

...То, что было мощной живой традицией в СССР в 1960-1980-е, сегодня -- полузабытые учебники, в основном уже потерянные, отдельные семинары и крохотная горстка исследователей, физически на 98% за нашими границами. Мир ушёл вперёд, и Россия в этой области даже не пытается догонять хотя бы для вида... И это, пожалуй, ещё грустнее, чем в случае с лямбда-исчислением: там советская школа хотя бы не участвовала в гонке. Здесь же участвовала и была впереди, но сошла с дистанции.

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