Добро пожаловать на канал MB3R Lab!

Меня зовут Анатолий Красновский. Я исследователь, работающий на стыке Computer Science, теории управления и системной инженерии. Этот канал посвящен применению формальных методов, теории систем и других аппаратов для анализа и проектирования сложных вычислительных систем.

Мы живем в мире, где отказ одного микросервиса может обрушить целую экосистему, а «галлюцинация» нейросети — поставить под сомнение доверие ко всей технологии. Простого тестирования и интуитивных решений для систем такого масштаба уже недостаточно.

О чем этот канал?

В современной IT-индустрии мы наблюдаем, как фундаментальные концепции, пришедшие из академической науки стремительно адаптируются практикой. Зачастую в этой гонке за быстрым внедрением их формальное, математическое ядро размывается, а сами термины превращаются в набор эвристик и «лучших практик». Возникает опасный разрыв между тем, что мы строим, и тем, как глубоко мы это понимаем.

Миссия этого канала — наводить мосты через этот разрыв. Мы будем говорить о важности формализма и не только. Не как об абстрактной самоцели, а как о мощнейшем инструменте для создания по-настоящему предсказуемых, верифицируемых и надежных систем. Речь пойдет о том, как строгий академический подход и математическое моделирование позволяют перейти от реактивного «латания дыр» к проактивному проектированию архитектур, чьи свойства можно доказать, а не только проверить.

Здесь я буду делиться своими исследованиями, аналитическими заметками и идеями. Рад видеть здесь коллег-исследователей, инженеров и всех, кто проектирует и эксплуатирует сложные системы.

Тирания «лучших практик»: почему мы строим карго-культы вместо надежных систем

В любой инженерной дискуссии рано или поздно звучит фраза-оберег, способная остановить любой спор: «Это лучшая практика». Это словосочетание — своего рода индульгенция. Оно освобождает от необходимости думать, анализировать контекст и брать на себя ответственность за принятое решение.

Аэропорты из бамбука и кластеры Kubernetes

В середине XX века был описан феномен «карго-культа» у меланезийских племен. Во время WWII там располагались военные базы, и аборигены видели, как с неба прилетали огромные «птицы» и привозили консервы и одежду. Когда война закончилась, самолеты перестали прилетать.

Чтобы вернуть их, племена начали воспроизводить ритуалы, которые они наблюдали у солдат: строили из бамбука и соломы копии диспетчерских вышек, самолетов. Маршировали с деревянными «ружьями». Самолеты, конечно, не вернулись.

А теперь посмотрим на IT-индустрию. Netflix добился успеха с микросервисами — и команды по всему миру бросились распиливать монолиты. Google написал SRE-гайд — и компании начали нанимать SRE, часто превращая это в ритуал, а не в инструмент улучшений.

Мы строим взлетно-посадочные полосы из Kubernetes, возводим вышки из Prometheus и ждем «карго» в виде надежности. Но оно не прилетает. Потому что мы копируем ритуал, а не фундаментальные принципы, сработавшие в совершенно ином контексте.

Контекст — это не деталь. Контекст — это всё.

«Лучшая практика» по своей природе игнорирует контекст. Это решение для конкретного набора проблем, ресурсов и масштаба. Вырванная из этого контекста, она перестает работать. Она предлагает простой ответ на сложный вопрос, поощряя интеллектуальную лень.

Авторитет как алиби

Второй столп карго-культа — это апелляция к авторитету. Но зачастую «лучшая практика» или методология — это не просто знание, а коммерческий продукт, окруженный экосистемой из тренингов и консалтинга. Автор, продвигающий свой фреймворк, заинтересован не в решении вашей проблемы, а в убеждении вас в универсальности своего метода. Поэтому первый вопрос к любому новому подходу — это классическое «Cui bono?». Часто ответ на этот вопрос помогает отделить реальный инженерный опыт от грамотно упакованного инфопродукта.

Призрак доказательной инженерии

Что же делать? В начале 2000-х годов в академической среде был дан интересный ответ, вдохновленный доказательной медициной. Это была попытка создать Evidence-Based Software Engineering (EBSE), или «доказательную программную инженерию». Идея была в применении научного метода: основывать выбор технологий не на фольклоре, а на измеряемых данных и результатах контролируемых экспериментов.

Почему же этот подход не стал отраслевым стандартом? Ответ прозаичен: это сложно, долго и дорого для коммерческих компаний, живущих в бешеном ритме релизных циклов. Индустрия просто не смогла (и не захотела) замедлиться, чтобы внедрить этот подход в его первозданном виде. Движение EBSE так и не стало мейнстримом.

И все же, тот факт, что EBSE как формальное движение не взлетело, не отменяет правоты его основной идеи. Наоборот, сегодня эта идея важна как никогда, но для ее реализации требуются другие инструменты. Если в 2000-х речь шла в основном о статистическом анализе полевых исследований, то сегодня у нас есть нечто более мощное:

- Формальное моделирование систем и их свойств.
- Симуляции и цифровые двойники, позволяющие проводить тысячи экспериментов без риска для продакшена.
- Продвинутый анализ данных и каузальный вывод, способные находить не просто корреляции, а причинно-следственные связи в поведении сложных систем.

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

Заключение

Цель этого поста — не отвергнуть весь накопленный индустрией опыт. Цель — призвать к интеллектуальной честности. Настоящая «лучшая практика» только одна — это привычка к критическому мышлению и принятию решений на основе доказательств.

Готовим статью о русскоязычной инженерной терминологии вокруг resilience и обосновании отдельного термина «резилентность». Нужна обратная связь практиков, чтобы опереться не только на библиометрию, но и на реальное поле.

Что хотим узнать
— Какие русскоязычные формулировки сейчас используются вместо resilience (устойчивость, живучесть, робастность, отказоустойчивость и др.).
— Как это влияет на постановку требований, метрики (MTTR/SLO/SLA), дизайн отказов и восстановление.
— Насколько «устойчивость» понимается однозначно в инженерных командах и где возникает путаница со stability/sustainability.
— Готовность сообщества поддержать выделение отдельного термина «резилентность» для описания способности системы переживать нарушения и возвращаться к приемлемому уровню работы.

Кому адресован опрос
— DevOps, SRE, системные архитекторы, инженеры платформ/инфраструктуры, разработчики, QA, руководители команд.

Как устроено
— 4 коротких вводных вопроса.
— 8 коротких вопросов по делу, \~1–2 минуты.
— Можно проходить с десктопа и телефона.

Конфиденциальность и использование данных
— Анонимно: никаких e-mail/ФИО не собираем.
— Данные пойдут только в агрегированную статистику.
— Результаты войдут в статью и публичную сводку рекомендаций для документации/ТЗ; сводку опубликуем в канале.

Форма: https://forms.yandex.ru/cloud/6899feb8eb61464f73ca92ac

Поможете делу, если перекинете ссылку в профильные чаты/команды.

Если у вас есть яркий пример, где «устойчивость» была понята по-разному и это повлияло на решение или метрики, обязательно опишите его в свободном поле в конце опроса — такие кейсы особенно ценны. Спасибо!

"Это кто тут наследил?" Учимся читать «отпечатки» системы

Как сравнить системы на надёжность, ещё на этапе проектирования? Можно спорить, опираясь на опыт и интуицию (о да, всё как мы любим). А можно и посчитать. Для этого уже четверть века существует и развивается элегантный математический аппарат — теория сигнатур (статья, книга).

Что это такое?

В надёжности «сигнатура когерентной (монотонной) системы» формально определена. Доказаны представление надёжности через порядковые статистики компонентов, инвариантность сигнатуры к конкретным распределениям (при стандартных предпосылках), есть результаты про композицию модулей и обобщение на разнотипные компоненты. Это не эвристика и не «школа мнений», а оформившаяся ветка теории надежности.

Если коротко, сигнатура — это «профиль надёжности» системы, выраженный в виде простого вектора. Допустим, есть система из n одинаковых компонентов. Её сигнатура — это вектор (s₁, s₂, ..., sₙ), где sᵢ — это вероятность того, что вся система упадёт именно в тот момент, когда откажет i‑й по счёту компонент.

Два наиболее очевидных примера:

— Последовательная цепь: сервисы вызывают друг друга по цепочке. Всё ломается при отказе любого из них. Сигнатура такой системы: (1, 0, 0, ...). Вся вероятность отказа — на первом же шаге.

— Полное резервирование: n реплик сервиса работают параллельно. Система держится, пока жива хотя бы одна. Сигнатура: (0, 0, ..., 1). Вероятность отказа — только на самом последнем компоненте.

Сигнатура показывает, как быстро конструкция деградирует. Чем сильнее вектор «сдвинут вправо», тем надёжнее система.

Зачем это нужно на практике?

Главная сила этого подхода — в объективности и простоте:

— Сигнатуры позволяют формально сравнить разные схемы отказоустойчивости (например, кворумы «2‑из‑3» против «3‑из‑5») и понять, какая из них на самом деле прочнее.

— Не нужны исторические данные о реальных отказах. Сигнатура зависит только от топологии — от того, как компоненты соединены между собой.

Это даёт инженерам простой и однозначный способ говорить о структурной надёжности, подкрепляя решения математикой, а не эмоциями. Для более сложных случаев, когда компоненты в системе разнородные (например, разные типы сервисов), используется обобщение — сигнатура выживаемости (survival signature). Она учитывает не только порядок отказов, но и типы вышедших из строя компонентов.

И в чём подвох?

Конечно, это не «серебряная пуля». У классической теории сигнатур есть чёткие границы: она статична. Она ничего не знает про динамику реального мира — про таймауты, каскадные отказы, деградацию производительности, очереди запросов или адаптивное поведение системы. Её роль — служить дисциплинирующим первым шагом. Это мощный инструмент для анализа и сравнения архитектурных «эскизов» в их чистом, структурном виде.

Гибкие монолиты и где они обитают

Сегодня распределённые архитектуры априори считаются более надёжными: избыточность, георепликация, изоляция отказов, независимые релизы, частичная деградация, быстрый откат — всё это снижает MTTR и удерживает SLO даже при частичных отказах. Это закреплено в «математике доступности»: A = MTTF/(MTTF + MTTR), а снижение MTTR (авто‑митигация, быстрый роллбек) повышает A. Практики SRE прямо оптимизируют MTTR, чтобы выдерживать SLO.

В больших организациях и глобальном трафике распределёнка объективно удобнее: масштабирование по географии, по нагрузке, по доменам. Монолит здесь часто упирается в организационные границы, темп релизов и физику одного процесса/БД. А распределённые системы проектируются, принимая во внимание компромиссы согласованности, отказоустойчивости и латентности.

Следите за руками. Что если сделать шаг в сторону и посмотреть на это, как на механику? В частности, как на эти два класса механизмов:

Классические механизмы — шестерни, шарниры, подшипники. Надёжность упирается в трение, люфты, загрязнение, допуски. Каждый узел вводит свою вероятность отказа, а суммарная надёжность пути для «чисто серийной» структуры равна произведению надёжностей узлов. Чем больше сочленений, тем ниже общий RR и короче ресурс между отказами. Для роликовых подшипников это ограничение проявляется как контактная усталость и конечный ресурс — классика расчёта срока службы.

Гибкие (Compliant) механизмы — цельные (буквально монолитные) конструкции, где движение рождается за счёт упругой деформации. Нет трущихся пар, следовательно почти нет износа, нет смазки, меньше компонентов, меньше концентраторов напряжений. В инженерной литературе это прямо формулируется как преимущества: «нет износа, нет люфтов и нет трения» (для рабочих амплитуд в пределах упругости), уменьшение числа деталей и сборочных допусков. В ряде приложений флексуры при корректном выборе материала/геометрии достигают практически бесконечного срока — если максимальные напряжения ниже предела выносливости.

И тут напрашивается такая аналогия:

Монолит — гибкий:
— Единый процесс и адресное пространство — минимум «сетевых шарниров».
— Инварианты локальны: границ меньше, контрактов меньше, поверхностей отказа меньше.
— «Износ» — это усталость «материала» системы (память, GC‑паузы, ресурсы ОС), а не эрозия API между сервисами.
— Надёжность растёт за счёт уменьшения числа последовательных узлов на критическом пути.

Распределёнка — ригидная:
— Шарниры = RPC/сеть (HTTP/gRPC, брокеры, балансировщики).
— Трение = латентность и джиттер; «износ» = таймауты, ретраи, пики повторов, эволюция контрактов.
— Люфты = несовместимость версий; вибрации = пиковые нагрузки, очереди, хвостовые задержки (p99/p999).
— Надёжность пути падает с каждым дополнительным вызовом; MTTR компенсируется операционными практиками (автоскейл, перезапуски, кворумы, деградация).

Вопрос. Если смотреть через призму «гибких механизмов», можем ли мы сознательно проектировать монолиты так, чтобы выигрывать в MTTF без обязательного роста MTTR? Например:
— Формировать «внутренние флексуры»: чёткие модульные границы внутри процесса, локальная асинхронность (in‑proc очереди), явные инварианты доменов.
— Держать «рабочую амплитуду» деформаций: ограничивать сложность критического пути, контролировать хвостовые задержки и бюджет памяти/CPU как предел усталости.
— Выносить настоящие «шарниры» только на внешний периметр — и там инвестировать в контрактные тесты, обратную совместимость и деградацию.

Где та самая седловая точка, после которой появление шарнира становится неизбежным, а где цельность даёт фундаментальный запас надёжности? Что мы увидим, если спроектируем системы как «гибкие механизмы» — и поднимется ли их надёжность на новый уровень?

Handbook of Compliant Mechanisms, An Introduction to Flexure Design

Чего только не придёт в голову, пока валяешься с ангиной.

Correct-by-Construction и AI — от элитарной дисциплины к инженерной практике

В 1960-х Дейкстра писал о том, что тестирование может показать наличие ошибок, но не их отсутствие. Формальные методы обещали решить эту проблему радикально: доказать корректность программы математически, превратив разработку ПО из ремесла в строгую инженерную дисциплину. Системы вроде Specware из Kestrel Institute реализовали этот подход в виде correct-by-construction парадигмы, где код генерируется из формальной спецификации через цепочку доказуемо корректных refinement-шагов.

Представьте процесс: вы описываете систему, затем пошагово уточняете спецификацию, превращая абстрактные требования в конкретные алгоритмы. Каждый шаг сопровождается формальным доказательством того, что новая спецификация эквивалентна предыдущей. В конце этой цепочки система автоматически генерирует код, который по построению не может нарушить заданные инварианты.

Звучит как идеальное решение проблемы надежности ПО. Почему же мы не пишем так весь софт?

Потому что цена этого подхода была запредельной. Формальная спецификация требовала глубокого понимания логики высших порядков и теории категорий. Процесс refinement был мучительно трудоемким — каждый шаг детализации требовал ручного конструирования доказательств. Инструменты помощи существовали, но оставались примитивными. В результате формальные методы застряли в узкой нише критически важных систем — там, где цена ошибки измеряется человеческими жизнями или катастрофическими последствиями для безопасности.

Сдвиг парадигмы

Сегодня ситуация меняется фундаментально. Появление достаточно мощных AI-агентов создает возможность для радикального снижения барьера входа в формальные методы. Речь не о замене инженера, а о перераспределении когнитивной нагрузки.

Рассмотрим процесс correct-by-construction разработки как композицию двух принципиально разных типов задач. Первый тип — стратегический: декомпозиция проблемы, выбор инвариантов, определение архитектуры refinement-шагов. Это требует глубокого понимания предметной области и остается прерогативой человека. Второй тип — тактический: перевод неформальных требований в строгие логические формулы, конструирование доказательств, проверка консистентности спецификаций. Именно здесь AI-агенты могут взять на себя львиную долю работы.

Прогресс в этой области впечатляет. В 2018 году нейронные сети начали применять к execution-guided program synthesis, демонстрируя способность генерировать программы с учетом спецификаций. В 2023-м система Baldur показала, что LLM могут генерировать целые доказательства корректности для Isabelle/HOL за один проход, автоматически доказав 65.7% теорем из бенчмарка — на 8.7% больше, чем предыдущий state-of-the-art. К 2024 году появилась FVEL — интерактивная среда формальной верификации, которая трансформирует код в Isabelle и использует LLM для автоматического theorem proving, замыкая цикл от кода к формальной спецификации и обратно.

Новая экономика верификации

Это меняет экономику формальной верификации. То, что раньше требовало команды специалистов с PhD и месяцев работы, может быть выполнено инженером с базовым пониманием формальных методов и AI-ассистентом за недели. Порог входа снижается не до нуля — понимание того, что вы хотите доказать, остается необходимым — но до уровня, при котором формальные методы становятся экономически оправданными для более широкого класса систем.

Мы получаем возможность применять correct-by-construction подход не только к ядрам криптографических библиотек, но и к критическим компонентам распределенных систем, протоколам консенсуса, контроллерам в робототехнике — везде, где цена ошибки высока, но не настолько, чтобы оправдать текущую стоимость формальной верификации.

Это не означает, что формальные методы станут мейнстримом завтра. Они по-прежнему требуют иного мышления, иной культуры разработки. Но впервые за десятилетия появляется реальная возможность сделать доказуемо корректное ПО не элитарной дисциплиной, а инженерной практикой.

Вопрос не в том, произойдет ли этот сдвиг. Вопрос в том, как быстро.

Модельный коллапс IT

В сфере генеративного ИИ активно обсуждается феномен "модельного коллапса" (AI models collapse when trained on recursively generated data). Суть его в том, что когда новые поколения языковых моделей обучаются преимущественно на данных, сгенерированных предшественниками, распределение данных деградирует. Модель начинает "забывать" тонкие нюансы, теряет разнообразие и замыкается в цикле самореференции, становясь все более посредственной.

Не происходит ли нечто подобное в самой IT-индустрии, где "обучающим набором" служат не тексты, а идеи, практики и решения?

Эрозия разнообразия идей

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

Индустрия разработки программного обеспечения демонстрирует признаки, подозрительно схожие с деградацией данных:

1) Синтетические "лучшие практики".
На индустриальных митапах и конференциях обсуждаются субъективные взгляды на решение проблем, которые, будучи оторванными от глубокого анализа, становятся "синтетическими данными" для всей индустрии. Эти практики, не подкрепленные строгим формализмом, многократно пересказываются и адаптируются, теряя связь с первоначальным контекстом и глубиной. Отсутствие формальных методов в широкой практике является одной из причин, по которой неформальные "best practices" остаются субъективными и не поддаются строгому анализу (Investigating the Homogenization of Web Design: A Mixed-Methods Approach).

2) Деградация разнообразия идей.
Когда инженеры "варятся в собственном соку", пересказывая друг другу одни и те же "паттерны", происходит потеря разнообразия. Утрачивается связь с первоисточниками — основополагающей информатикой, теорией систем, строгими инженерными дисциплинами. Этот процесс ведет к гомогенизации инструментария и подходов, что уже фиксируется в исследованиях (Formal methods: Practice and experience). Сообщество начинает обучать само себя на собственном, все более гомогенном и поверхностном "опыте".

3) Монополия на парадигмальные сдвиги.
В результате, парадигмальные сдвиги приходят почти исключительно из BigTech. Отчеты показывают, что значительная часть роста R&D (до 78%) приходится именно на крупные технологические компании (Tip of the Iceberg: Understanding the Full Depth of Big Tech’s Contribution to US Innovation and Competitiveness), что подтверждает их доминирование в поставке принципиально новых знаний. Остальная часть рынка лишь потребляет и адаптирует эти решения, не создавая новых.

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

Конечно, аналогия не абсолютна. IT-индустрия обладает механизмом обратной связи в виде сбоев в продакшене и финансовых потерь. Однако этот механизм является реактивным, а не проактивным, и не способен остановить медленную, но неуклонную эрозию основополагающих знаний.

Кризис основополагающих знаний

Этот кризис усугубляется появлением "ИИ-слопа" (AI-slop) — низкокачественного, гомогенного кода, сгенерированного инструментами на базе LLM. ИИ-слоп, будучи продуктом "модельного коллапса" в чистом виде, становится новым, массовым источником "синтетических данных" для будущих поколений инженеров и моделей.

Индустрия рискует превратиться в гигантскую и неэффективную языковую модель, которая генерирует все более посредственный код, обученный на собственных, синтетических "лучших практиках" и усугубленный повсеместным ИИ-слопом.

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

Эмерджентность как критерий архитектурной адекватности


Инженерная культура по-прежнему опирается на картезианский принцип: «раздели сложное на части, чтобы понять его». Мы проецируем это на архитектуру, полагая, что статическая декомпозиция (DDD, SRP или «архитектурные кванты») гарантирует предсказуемость системы.

Однако в распределенных средах мы упираемся в барьер, описанный нобелевским лауреатом Филипом Андерсоном в статье More Is Different: способность свести всё к фундаментальным компонентам не дает возможности реконструировать поведение целого. Количество переходит в качество, порождая эмерджентность.

Почему Теория Систем применима к ИТ?
Л. фон Берталанфи в General System Theory вводит понятие логической гомологии: системы разной природы (клетки или микросервисы) подчиняются одинаковым законам, если они являются «комплексом взаимодействующих элементов». Проекция здесь прямая: в ИТ существуют свойства, зависящие от топологии связей, а не от кода компонентов.

Научный базис, от статики к CAS
Это не просто теория 60-х. Современная наука о Software Engineering (SE) активно подтверждает этот сдвиг, рассматривая микросервисные архитектуры как Complex Adaptive Systems (CAS).

1. Antifragility vs. Robustness. Исследование M. Monperrus Principles of Antifragile Software математически аргументирует, что классическая отказоустойчивость (попытка избежать ошибок на этапе Design Time) менее эффективна, чем архитектура, способная обучаться на сбоях в динамике.
2. Runtime Adaptation. Сообщество SEAMS (Software Engineering for Adaptive and Self-Managing Systems) в своей фундаментальной работе Software Engineering for Self-Adaptive Systems: A Research Roadmap утверждает: поскольку предсказать эмерджентное поведение заранее невозможно, архитектурные решения должны мигрировать в рантайм.
3. Microservices as CAS. Свежие работы, например Self-Adaptive Microservice-based Systems - Landscape and Research Opportunities, показывают, что попытки управлять микросервисами через жесткую оркестрацию проигрывают хореографии и самоадаптации.

Анатомия эмерджентности в коде
Если принять этот изоморфизм, эмерджентность становится конкретным классом инженерных проблем:

—Нелинейная латентность. Сервис А и Сервис Б отвечают за 50 мс. Но в системе с очередями общая задержка определяется не суммой, а законами теории массового обслуживания (Little's Law) и стохастикой потока.
—Резилентность. Локально корректный паттерн retry внутри компонента при масштабировании превращается в Retry Storm. Свойство «надежность компонента» при взаимодействии трансформировалось в эмерджентное свойство «нестабильность системы».

Interaction Design как смена парадигмы
Для открытых систем (которыми является любой HighLoad) изучение их морфологии (границ, классов) недостаточно для понимания их физиологии (процессов).

Адекватная архитектура — это проектирование взаимодействий. Мы должны управлять эмерджентностью через механизмы, не имеющие смысла для одиночного сервиса: Circuit Breakers (разрыв вредных обратных связей), Backpressure (управление потоком) и Consensus Protocols.

Пока мы оцениваем архитектуру только по красоте декомпозиции, мы занимаемся анатомией. Живая архитектура находится в пространстве «между» — там, где рождается поведение.

Cogito, ergo sum
В самом фундаменте картезианства скрыта глубокая системная ирония. Декарт опирался на Cogito как на неделимую точку опоры. Но сегодня мы понимаем: Cogito («я мыслю») — это эмерджентное свойство нейронной сети, результат сложнейшего взаимодействия миллиардов клеток.

Следовательно, Sum («я существую») — это не просто факт наличия биологической материи, а констатация существования системы как целого.

И здесь кроется ключевой инсайт: эмерджентное свойство является критерием существования системы. Пока нет «мышления», нет никакого «Я» — есть лишь набор разрозненных биологических компонентов. Система начинает существовать как система только тогда, когда проявляется её эмерджентное свойство.

Иллюзия непрерывности: вычислительная устойчивость как скрытый фундамент

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

Современный разработчик привык жить в мире идеальной платоновской математики. Мы пишем x = y + z и полагаем, что оперируем числами из множества R (вещественные числа). Но компьютер — это дискретная машина. Он ничего не знает о непрерывности и оперирует конечным множеством представимых значений (часто IEEE 754), а каждая операция — это ещё и правило округления/обрезания..

На этой скользкой дорожке пролегает опаснейший разрыв: карта перестаёт соответствовать территории. О том, насколько глубока эта кроличья нора, Дэвид Голдберг написал еще в 1991 году в своей канонической работе What Every Computer Scientist Should Know About Floating-Point Arithmetic — чтиво, обязательное для каждого, кто вышел за пределы integer.

Что такое устойчивость алгоритмов?
В строгом смысле, как это формулирует Николас Хайем в фундаментальном труде Accuracy and Stability of Numerical Algorithms, алгоритм считается вычислительно устойчивым, если ошибка на выходе («шум» вычислений) сопоставима с ошибкой, вызванной возмущением входных данных. Проще говоря: если вы слегка толкнули входные данные, результат не должен улетать в стратосферу.

Аналогия из теории управления и механики. Представьте, что ваш алгоритм — это механическая система.
Устойчивый алгоритм — это шарик на дне чаши. Любая погрешность округления (гравитация) возвращает его к истинному значению. Ошибки затухают (dampening).
Неустойчивый алгоритм — это перевернутый маятник или карандаш, балансирующий на острие. Малейшее дыхание хаоса (округление в 16-м знаке после запятой) порождает положительную обратную связь. Ошибка не просто накапливается — она экспоненциально усиливается на каждом шаге итерации.

Эффект бабочки в FPU
Это не теоретическая проблема. Это проблема физики вычислений, которая стоит жизней.

1) Хрестоматийный пример, Patriot в Дахране (1991). Система держала время в десятых долях секунды и конвертировала его в секунды с ограниченной разрядностью, что давало микроскопическую погрешность на каждой итерации, но при длительном аптайме она нарастала. После ~100 часов непрерывной работы ошибка составила ~0.3433 с, а смещение окна ~687 м. В результате батарея не смогла корректно сопровождать цель и не произвела перехват. Scud попал в казарму, погибло 28 человек.

2) AI и взрывающиеся градиенты. В обучении глубоких нейросетей мы постоянно боремся с числом обусловленности (Condition Number) матриц. Если ландшафт функции потерь имеет «овраги» с крутыми склонами, обычный градиентный спуск становится вычислительно неустойчивым — веса улетают в NaN.

Инженерный вывод
Мы часто путаем математическую корректность формулы и вычислительную устойчивость алгоритма, её реализующего.

Математически a+(b+c)=(a+b)+c.
Вычислительно — нет.
Порядок операций имеет значение. Суммирование ряда чисел от меньшего к большему или использование алгоритма Кэхэна даёт один результат, а хаотичное суммирование — другой, зачастую с потерей значимости (catastrophic cancellation).

Проектируя сложные системы — будь то финансовый биллинг, физический движок или ML-модель — мы должны смотреть на алгоритмы не как на статические формулы, а как на динамические системы, через которые протекает поток данных. И главный вопрос, который стоит задать: является ли ваша система диссипативной или она резонирует от собственного шума округления?

N.B. В русскоязычном пространстве мы попадаем в любопытную семантическую ловушку. Мы используем слово «устойчивость» для перевода сразу двух фундаментально разных (или нет?) понятий: Numerical Stability (свойство алгоритма не накапливать ошибку) и Resilience (способность системы адаптироваться к сбоям).

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

Инварианты Шрёдингера

Мы привыкли считать Domain-Driven Design золотым стандартом для защиты бизнес-логики. Агрегаты, Value Objects, сущности — весь этот инструментарий направлен на то, чтобы удерживать критические инварианты внутри границ агрегата и минимизировать пространство несогласованных состояний.

Мантра звучит успокаивающе: «Валидируй на входе, защищай границы, и всё будет хорошо». Гарды в конструкторах, исключения кидаются. Спим спокойно.

Однако с точки зрения теории типов и формальных систем, этот подход зиждется на двух фундаментальных допущениях, которые при ближайшем рассмотрении оказываются иллюзорными.

1) Булева слепота (Boolean Blindness).
Когда вы пишете if (isValid(email)) { ... } else { throw ... }, вы создаёте эфемерное свидетельство, которое не переживает область видимости.

Внутри блока if вы знаете, что данные корректны. Но для компилятора (и для структуры памяти) этот объект остаётся просто строкой. Вычислительная информация расщепляется: значение живёт отдельно, а факт его валидности стирается сразу после закрывающей скобки. Система «слепнет».

Это заставляет нас строить бюрократию из защитного кода, вместо того чтобы пользовать физику типов. Настоящая защита — это подход Parse, don’t validate, где недопустимые состояния становятся непредставимыми (unrepresentable) структурно, а не просто запрещёнными императивно. Завозимая везде и всюду «функциональщина» — это не просто хайп.

2) Проблема фрейминга и крах локальности.
Но допустим, вы идеально реализовали Value Objects. Вы уверены, что Агрегат — это надёжная крепость, границы которой защищены инкапсуляцией.

Здесь нас поджидает не то, чтобы неожиданный, но неприятный факт, который обычно игнорируется в индустрии: в языках с общим изменяемым состоянием (Shared Mutable State) модульная верификация инвариантов практически неработоспособна без дополнительных логик.

Это обычно называют проблемой фрейминга/фрейм-условий (framing), которая становится особенно острой из‑за алиасинга в куче. Даже когда вы обвешали методы контрактами (Design by Contract), классическая логика Хоара не масштабируется без явных фрейм-условий, если ссылка на внутренности вашего Агрегата утекла наружу или была сохранена кем-то ещё.

Инвариант, который вы считаете локальным («сумма транзакций в этом списке < X»), на самом деле зависит от глобального состояния кучи (heap). Любой внешний актор, имеющий ссылку (alias), может изменить состояние в обход ваших гардов. В этот момент Агрегат продолжает «считать» себя валидным, хотя его внутренняя структура уже разрушена.

Separation Logic: недостающее звено

Чтобы абсолютно строго рассуждать об инвариантах в мутабельной среде, нам необходима Separation Logic (логика разделения), разработанная Рейнольдсом и О’Хирном. Она вводит понятие пространственного разделения ресурсов (P * Q), позволяя доказать, что изменения в одной части памяти не ломают инварианты в другой.

Без поддержки этой логики на уровне языка или верификатора, любой инвариант в классическом OOP/DDD является скорее вероятностным, чем строгим.

Что дальше?

Индустрия медленно, но верно движется от «деклараций о намерениях» к структурным гарантиям. Например Rust «встраивает» упрощённую версию Separation Logic в систему типов через механизм Ownership & Borrowing. Если вы владеете структурой, компилятор гарантирует отсутствие внешних мутабельных ссылок. Мутабельный алиасинг исключён, инвариант становится локальным и доказуемым. Но это только начало пути.

Агрегат в его нынешнем виде — это не крепость, а забор из сетки-рабицы. Настоящий Correctness-by-Construction начинается там, где мы перестаём полагаться на рантайм-проверки и начинаем контролировать топологию памяти.

Cui bono?

Экосистема Enterprise-разработки монетизирует процесс героической борьбы с энтропией, а не её устранение. Консультанты и евангелисты продают сложные лекарства от симптомов, которые возникают из-за фундаментальной слабости инструментов. Сделать систему верифицируемой — значит обрушить рынок «лучших практик», созданный для обслуживания её хрупкости.

Почему следующим рубежом AI станет формальная философия

Мы живем в удивительное время. Современные AI-агенты пишут код, генерируют сложные архитектурные драфты и, как мы уже обсуждали, способны автоматически доказывать теоремы в системах вроде Isabelle/HOL. Глядя на это, легко поддаться иллюзии, что до AGI осталось сделать буквально пару шагов.

Но на фоне этого великолепия нейросети продолжают феерически проваливаться на задачах, требующих банальной житейской смекалки — того, что Франсуа Шолле называет способностью к обобщению и адаптации (On the Measure of Intelligence).

Спросите передовую LLM, как налить чай в кружку, у которой запаян верх и отсутствует дно. Модель с умным видом начнет объяснять, что это топологически невозможно, представляя себе некую нерабочую трубу с заглушкой. Она не способна понять очевидную для любого ребенка вещь: это просто перевернутая кружка.

Или задайте вопрос: «Как лучше добраться до автомойки — поехать на машине или пойти пешком?». Алгоритм начнет взвешивать плюсы пешей прогулки для здоровья, забыв, что мыть пешехода на автомойке — так себе идея.

Синтаксис без семантики
В чем фундаментальная проблема? LLM — это виртуозные статистические машины. Они блестяще оперируют синтаксисом, выстраивая вероятностные цепочки токенов, но у них нет семантики реального мира.

У них нет концептуального понимания того, что такое «емкость», «пространственная ориентация» или «целеполагание». Сегодня главным узким местом технологического прогресса стала не вычислительная мощность, а способность алгоритма с полуслова понимать человека, его интенции и физические ограничения среды.

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

Оцифровка «здравого смысла»
Речь не о пространных рассуждениях о смысле жизни. Формальная философия — это строгий математический и логический аппарат для описания того, как устроен мир и наше знание о нем. Чтобы преодолеть этот «семантический барьер», нам потребуются конкретные разделы этой науки:

— Формальная онтология и мереотопология (теория частей, целого и границ). Как объяснить машине, что такое объект в пространстве? Кружка — это не просто набор токенов. Это физический объект, свойства которого зависят от его ориентации (гравитации). Без строгой онтологии пространства модель всегда будет путать перевернутую кружку со сломанной трубой.
— Эпистемическая и модальная логики. Аппарат для работы с концептами «знание», «необходимость» и «возможность». Это база для понимания намерений человека. Почему мы едем на автомойку? Логика позволяет выстроить строгую каузальную цепочку и принять, что пешком идти логически бессмысленно.
— Формальная прагматика. Переход от анализа слов к вычислению контекста. А как мы помним: контекст — это всё.

От гуманитарной рефлексии к системной инженерии
Попытки оцифровать «здравый смысл» (common sense) провались. Проекты вроде Cyc Дага Лената, пытавшиеся вручную описать миллионы логических правил, захлебнулись в собственной сложности. Здравый смысл оказался слишком гибким для классического программирования.

Но сегодня, когда у нас есть мощные нейросети, способные парсить неструктурированные данные, мы подошли к точке, где формальная философия превращается в прикладную инженерную дисциплину. Точно так же, как теория графов когда-то легла в основу маршрутизации сетей, аппарат формальной философии ляжет в основу World Models (моделей мира) для следующего поколения ИИ.

Мы больше не можем полагаться на то, что модель «выучит» физику и логику, просто прочитав весь интернет. Статистика пасует перед out-of-distribution задачами, где нужен дедуктивный вывод на основе свойств физического мира.

Чтобы перейти от блестящих имитаторов (стохастических попугаев) к агентам, способным надежно, предсказуемо и безопасно оперировать в реальном мире, нам придется научить машины философии. И тот, кто первым создаст масштабируемый, вычислимый аппарат для формализации здравого смысла, определит архитектуру следующей эпохи.