Зачитался свежаком "Compositional Program Verification with Polynomial Functors in Dependent Type Theory" (композиционная верификация кода на основе полиномиальных функторов в зависимой теории типов, формализована полностью в Agda!)

Так понял, это по сути мета-рецепт (категорная база) создания композиционных фреймворков верификации в самых разных сеттингах: меняешь моноидальное произведение -- получаешь конкурентность, меняешь категорию -- получаешь реляционную верификацию и т.д. Круто. По сути, затащили в целостную систему через зависимые полиномы давно известные фишки вроде полиномиальных функторов, свободных монад, триплов Хоара, Mealy-машин...

Для "Функциональных архитектур" прикинул уже штук пять следствий полезняшек, будем их разбирать как обычно в формате "вот тебе прикладные рекомендации применяй прямо сейчас, вся математика под капотом", примеры дам на шарпе или питоне.

Например, агент -- это программа в free-монаде (AST исполнения) над суммой инструментов, каждый из которых - интерфейс вход-выход, а спеку для него задаём пред/пост условиями. Фишка -- что верифицируем и тестируем только тулы, а не их комбинации, и при этом получаем свободно сменяемый рантайм. План вызовов агента делаем чистой структурой данных (дерево вызовов тулов), которая будет сущностью первого класса, которую можно исполнить, залогировать, прогнать в dry-run, в другой рантайм, закэшировать...

А в этом вашем любимом cli, пайп формализуем как композицию Клейсли с контрактами. Каждой утилите добавляем декларативную спеку, и простенькая обёртка проверяет совместимость пред/постусловий до запуска. Реализуется вообще просто: JSON Schema на stdin/stdout каждой команды, и статический чекер пайплайна.

На каждую такую штуку буквально достаточно пару сотен строк кода, сам агент/cli вообще трогать не надо, а имеем таким образом статическую проверку склеиваемости инструментов агентов до того, как нейронка сожжёт токены или испортит полпроекта :)

Главное — идти от математики, а не от инженерии, и тогда всё будет получаться ясно и естественно.