...В процессе изучения функциональных архитектур проявился такой совершенно неожиданный инсайт 💥 что в качестве языка формальных спецификаций вообще не нужны специализированные языки вроде tla, dafny, typespec, veil, loom/velvet! Последний кстати зафигачен на lean4, и с его помощью уже успешно перетаскивают код с dafny на лин. При том, что этот процесс бессмысленен :) Не так сложно написать даже просто алгоритмический код, который не выйдет полноценно верифицировать на dafny, а главное, что оно не имеет доступа ни к каким реальным библиотекам, то есть абсолютно далеко от реального прода.

Главное же, что даже крутые системы зав.типов от пруверов вроде Lean не нужны, а достаточно Хаскеля!!1 🚀

В целом я этот язык здорово недолюбливаю, в математическом смысле он местами сильно кривой, а для реальных проектов не подходит во многом по техническим причинам (хотя есть немало исключений). Но, блин, до чего же хороша его система типов! 💪🏻 Точнее, она прежде всего строгая, и тот же F# конечно от неё далёк. Нам не нужно искать и читать исходный код, чтобы узнать, эта функция чистая или нет: вы можете просто посмотреть на её тип! -> Int или -> IO Int !

Поэтому хаскеля по сути достаточно, чтобы формально думать о чём угодно в программировании, включая и архитектурный уровень! 😇 А огромный плюс, что всё же Haskell -- это немножечко мэйнстрим, и его сегодня вполне может освоить и легко и просто задействовать любой нормальный программист, причём конкретно для правильного рассуждения о своих прозаических повседневных задачках, и даже с учётом конкретного фреймворка! Ну и так как любой ввод-вывод в хаскеле -- это вызов внешних сишных функций, мы получаем вообще идеальные возможности для гладкой интеграции!

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

Так вот, сегодня наткнулся на вышеупомянутый loom/velvet, а там "Loom uses Monad Transformer Algebras." 🤘

Я знал, я знал!!1 )))

...Без понимания этой алгебры, ваш ум, искорёженный императивщиной и ООП, будет гуглить на каждом шагу "Is it possible to convert an IO Int into an Int ??" :)

p.s. Умненький читатель к этому моменту должен получить понимание, какая связь между "convert an IO Int into an Int", функциональной и гексагональной архитектурами.