Мы привыкли считать 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-разработки монетизирует процесс героической борьбы с энтропией, а не её устранение. Консультанты и евангелисты продают сложные лекарства от симптомов, которые возникают из-за фундаментальной слабости инструментов. Сделать систему верифицируемой — значит обрушить рынок «лучших практик», созданный для обслуживания её хрупкости.