Про важность формальных методов, или даже про важность правильной думательной машинки для некоторой (любой) технологии.

Например, мэйнстримовская модель k8s заточена под цель "продавать курсы/техподдержку" - cмотрите как здорово, декларативные манифесты, контроллеры, "просто задекларируй желаемое состояние, и система мгновенно и надёжно приводит себя в него", срочно внедряем - совершенно не учитывает вычислительные модели распределённых систем (разбираем на соответствующем треке). А тут надо понимать прежде всего асинхронщину, частичную готовность, когда команда на удаление ушла, а под ещё жив и доедает твой трафик,
или наоборот не готов его принимать,
или часть подов новой версии, а часть старой, и они могут так сосуществовать бесконечно,
а что kubectl apply прошёл успешно, так конвергенция может вообще не наступить из-за ошибок и т.д. и т.п.

Я к тому, что все эти массовые модели по любым практически технологиям поощряют "думать" в соответствующем контексте крайне криво, что приводит к мириадам потенциальных багов.

Например, думаем о кубере как о "едином оркестраторе", но когда API тормозит, etcd теряет кворум, поды зависают, контроллеры в бесконечном ретрае (что кстати в условно формальной модели k8s не баг а фича ахаха), оказывается что никто к этому не готов, потому что их приучили думать, что когда kubectl apply зелёный, это гарантия.

Всё больше думаю двинуть куда-нибудь в кибербез ибо ФСТЭК и ГОСТы (КИИ, СКЗИ, ВТС...), где ещё минимально остаются взрослые формальные подходы, и люди понимают, что напиши хоть миллион тестов, это вообще ничего не гарантирует кроме patch-and-pray и никак особо не приближает к системе, которая полностью корректна (по крайней мере, в отношении некоторой спецификации)...

Именно тут как раз и может дать невероятный буст метапрограммирование по Алану Кэю, в "Функциональных архитектурах" разбирал много уже. Одно дело сертифицировать 100500 строк говнокода на Java (это миллионы (если не десятки миллионов) строк доказательств на каком-нибудь lean4), и другое дело -- 150 строк DSL в соответствующем домене. Например, Calculus of Constructions я реализовал на F# где-то в сотне строк.

Хотя, как говорили мастера дзен,
Даже если я объясню, никто не поймёт.
Думаю, мне лучше промолчать в лесу...