...В принципе, для этого всего можно найти много близких аналогий: категорная дуальность (леммы -- это морфизмы в категории доказательств, функции -- морфизмы в категории типов), абстрактная интерпретация (доказательства - типа, спецификации; функции - типа, их реализации), Карри-Ховард конечно классика — да только нафига.

Как не было толку от хаскелеподобных подходов, так и нету, разве что совсем нишевые ниши вроде формальной верификации (например, из Lean в Rust), документирования кода через "контракты" (как в Eiffel/Dafny), ну и обучение конечно.
Для практики нужен язык как минимум с поддержкой зависимых типов, и чтобы он был распространён хотя бы как F#.

=

Короче говоря, резюме такое, что даже самая топовая на сегодня математика уровня филдсовских лауреатов пока что только-только пытается выбраться из детсадовских штанишек programming in small. Забавно смотреть, как математики изобретают велосипед, открывая для себя например гитхаб, где леммы распределялись между участниками как issues, с PR, а их доказательства проверялись через CI/CD )))

Взять нам у них нечего, а вот дать можем очень много.

=

Соответственно итоговая цель получается такая, что вместо утверждений Тао, по сути, по теме programming in large, что

- процесс выделения лемм (классов, функций) — это искусство
- декомпозиция — это не столько технический метод, сколь "думательная дисциплина"

мы должны получить такую базу:

- процесс выделения лемм (классов, функций) — это алгоритм
- декомпозиция — это не столько думательная дисциплина, сколько технический метод, причём реализуемый на быстром мышлении (прокачки скиллов не требуется).

Думаю, что тут пока вполне можно остановиться на ООАП по Бертрану Мейеру, усиленному моделью акторов по Алану Кэю и Карлу Хьюитту, и получить очень хороший практический результат. Для начала, первый шаг -- отшлифовать немного мой трек ООАП теоркатом, GADT и HoTT.

Закроем сейчас programming in small гомотопическими типами, и возьмёмся за финальную темку в программировании :)