Без заголовка

Я что-то вроде "динамической математики" нахожу в формальных системах - в строгих логических моделях. Точнее обычно это называется алгебры - набор операций над какими-то объектами. Конечно, эти алгебры описываются друг через друга. Абстрактные типа данных - это тоже алгебры. Но чтобы компактно выражать какие-то идеи, в какой-то момент возникает необходимость в формальной проверке эквивалентности разных моделей или их частей. Вот тут и есть затык ибо вся эта верификация весьма трудоемка. Т.е. фактически нужно постоянно продумывать и формализовывать (под)морфизмы из одних (под)моделей в другие. Ну и из этих (под)морфизмов конструировать более сложные морфизмы.