Поясняю за "математику как формальный набор правил комбинирования типов."

Тут можно бесконечно рассуждать, например,

про иерархии тайпклассов (хаскель, скала (база!), раст, все теорем-пруверы),

или про то, что они нафиг не требуются, когда есть рекорды с композицией, и особенно зависимые типы,

или про типы как сущности первого класса для метапрограммирования,

или про конструктивную унивалентность, как в rzk (чистый "hott как язык программирования"), который (вроде как) умеет вычислять результат транспорта вдоль гомоморфизмов с автоматическим переносом доказательств между типами,
и ad-hoc полиморфизм соответственно не нужен,

или про предпучковые топосы как моделирование структур, зависящих от времени,

или про рекурсивные схемы как N-кратная компактность кода, когда сама рекурсия становится типом данных (фикс поинт; читаете ГПиМММ? :)

и т.д.

Я движусь шажочками, по какой-то странной тропинке неведомо куда :) Стратегического пути тут быть не может просто потому, что меняется айтишка очень быстро.
Читаю святых cs, разное по мета-математике, в перспективе планирую (Meta) Principles Framework, но это очень далёкая перспектива, увы.

Собственно, "Функциональные архитектуры" уже сейчас дают x10 в токенах/времени даже если их просто поверхностно почитать-помедитировать,
полноценные применения всех рекомендаций ФА/DSL + Last Principles Framework должны дать ещё несколько десятков раз, ну а там посмотрим.

Выложу на днях в частности в ФА про доменно-специфическую гиперспециализацию и спеки в конъюнктивной нормальной форме, чтобы потенциально подвязать к этим темкам SAT-солверы.

Мне случалось видеть старцев, занимавшихся исключительно усиленным математическим [телесным в ор.] подвигом, и пришедших от него в величайшее самомнение, величайшее самообольщение. Душевные страсти их, гнев, гордость, лукавство, непокорство, получили необыкновенное развитие.
Свт. Игнатий Брянчанинов