Личная история о том, как двадцатилетняя мечта о математически доказуемом коде неожиданно стала ответом на главный вызов эпохи ИИ‑агентов.
Прелюдия: Genesis и поиски утраченного детерминизма
Двадцать лет назад у нас была утопическая мечта. Мы строили платформу разработки под названием Genesis. Наша цель звучала амбициозно до наивности: загнать процесс написания кода в такие строгие рамки, чтобы код стал математически доказуемым, а архитектурные решения формировались из накопленного опыта системы, а не рождались в хаосе человеческих импровизаций.
Тогда мы придумывали свои термины, но нас никто не понимал. Само понятие «контрактное программирование» нам было не знакомо, уже после длительных переговоров, нам приходилось искать статьи Википедии, просто чтобы найти нужные слова и говорить с индустрией на одном языке. Мы искали грааль детерминизма, но инструменты того времени были к этому просто не готовы.
Времена радикально изменились. Но парадокс в том, что эти старые, почти забытые идеи стали актуальны как никогда. Только теперь жесткие рамки и контракты нужны не для того, чтобы ограничивать человека‑программиста, а для того, чтобы обуздать эту еб@нашку хаотичную, генеративную мощь искусственного интеллекта.
Мы не просто вернулись к старой мечте. Мы вынуждены были изобрести контрактное программирование заново — для новой реальности.
От написания кода к проектированию границ: почему главный навык разработчика в эпоху ИИ — это управление энтропией
Еще пять лет назад главным барьером в разработке было «трение синтаксиса»: необходимость помнить особенности языка, писать шаблонный код и вручную связывать модули. Сегодня ИИ‑агенты научились не просто предлагать следующие строки кода, но и анализировать репозитории, писать тесты и рефакторить модули.
Казалось бы, мечта сбылась. Но на практике команды сталкиваются с новой, более коварной проблемой. Если агент становится основным автором локальной логики, что именно остается делать инженеру? И почему внедрение ИИ в сложных проектах часто приводит не к ускорению, а к хаосу?
Феномен «операционной энтропии»
Проблема не в том, что ИИ плохо пишет код. Проблема в том, что реальные корпоративные системы редко дают ИИ четко ограниченную задачу.
Требования меняются на лету, схемы данных эволюционируют, а часть критически важных бизнес‑правил существует только «в чьей‑то голове» или в неформальных обсуждениях. ИИ‑агент, лишенный этого скрытого контекста, начинает опираться на устаревшие предположения. Он исправляет следствие, а не причину, или генерирует код, который технически работает, но противоречит общей архитектуре.
Это и есть операционная энтропия: накопление старых предположений, разветвляющийся контекст и нерешенные зависимости, которые делают поведение ИИ непредсказуемым. Агенты создают движение, но превращает ли система это движение в полезную и безопасную работу? Часто — нет.
Новая роль инженера: архитектор ограничений
В этих условиях ценность разработчика смещается. Вклад инженера больше не заключается в ручной трансформации требований в код.
Новая задача инженера — создавать границы, которые делают ошибку агента видимой, конкретной и исправимой.
Разработчик превращается в архитектора систем обратной связи. Его работа — проектировать правила, внутри которых ИИ может действовать автономно, но за пределами которых система немедленно подает сигнал тревоги. Это переход от роли «писателя кода» к роли «валидатора и дирижера» интеллектуальных агентов.
Чего не хватает современным инструментам?
Текущий стек инструментов для ИИ‑разработки сфокусирован на генерации, но катастрофически слаб в вопросах доверия и трассируемости.
Чтобы ИИ‑кодинг стал надежным стандартом для продакшена, индустрии необходим новый концептуальный слой между постановкой задачи и выполнением. Инструменты будущего должны предоставлять разработчикам:
Контракты намерений. Механизм, позволяющий формализовать не только что нужно сделать, но и какие ограничения при этом нельзя нарушать, и как будет проверяться результат.
Сквозную трассируемость. Возможность в любой момент времени ответить на вопрос: «Почему агент принял именно это архитектурное решение?» и отследить цепочку от бизнес‑требования до конкретной строки кода.
Неизменяемые журналы доказательств. Локальные, верифицируемые логи, которые фиксируют не просто факт генерации кода, а контекст, проверку гипотез и результаты валидации.
Детерминированные процессы проверки. Создание условий, в которых сгенерированной логике можно доверять, потому что она прошла через строгий семантический фильтр, а не просто «выглядит рабочей».
Будущее уже здесь, оно просто неравномерно распределено
Ценность разработки программного обеспечения не исчезает по мере того, как генерация кода становится дешевле. Она просто поднимается на уровень выше.
Компании, которые смогут первыми построить культуру и инструментарий для управления ИИ‑агентами через строгие границы и верифицируемые контракты, получат колоссальное преимущество в скорости и качестве. Остальные же утонут в операционной энтропии, бесконечно исправляя галлюцинации своих же помощников.
Главный вопрос на ближайший год звучит не «Насколько умным станет ИИ?», а «Насколько надежными станут системы, которые мы строим для управления этим ИИ?».
От теории к практике
Для меня эта статья — не просто размышление о будущем индустрии. Это фиксация пути, который мы прошли и который продолжаем идти.
Идеи, описанные выше — контракты намерений, трассируемость от бизнес‑требования до строки кода, локальные журналы доказательств, детерминированная валидация — перестали быть для нас абстракцией. Они стали ядром продукта, который мы строим под названием Work Graph.
Многое из того, о чем я писал, уже работает. Мы создали ядро, которое позволяет задавать ИИ‑агентам строгие границы, фиксировать их действия в виде верифицируемых цепочек и сохранять полный контекст принятия решений — локально, в репозитории, без отправки данных в облако. Мы используем этот инструмент на собственных проектах и видим, как он меняет сам подход к работе с ИИ: от хаотичной генерации к управляемому процессу.
Что в разработке?
Сегодня Work Graph отлично управляет задачами, файлами и свидетельствами. Он знает, что агент сделал, и может это проверить. Но между «человек сформулировал намерение» и «агент написал код» всё ещё остаётся пространство, в котором живёт операционная энтропия.
Мы спроектировали следующий слой — когнитивный компилятор, который превращает бизнес‑правило в проверяемый граф операций ещё до того, как будет написана первая строка кода. Это мост между естественным языком и математически доказуемой логикой. Граф, который можно верифицировать, исполнить детерминированно, скомпилировать в любой язык программирования — от TypeScript до 1С — и при этом быть уверенным, что ни одно бизнес‑правило не потерялось по дороге.
Комментарии (18)
Politura
01.09.2026 18:33Чего не хватает современным инструментам?
Перестать делать "херак-херак и в продакшен". Натренированные на тоннах индусского кода, когда зп или промоушен видимо зависел от количества строчек кода, а не от его смысла, все эти Опусы зачастую стараются сильно переусложнять код. Правильное слово overengineering, хз как это по-русски сказать. И как вы с этим собираетесь бороться? Работать-то оно работает.
diflux Автор
01.09.2026 18:33Следующий шаг Work Graph — стать генеративным Low-Code. Overengineering становится просто невозможным: если решение можно собрать из существующих кирпичиков — ИИ обязан использовать их, а не изобретать велосипед.
Сложность появляется только тогда, когда она действительно оправдана и чтобы создать что-то новое, ИИ должен пройти процесс: написать контракт, тесты и пройти валидацию, которая математически проверяет связность и минимальность.
evgeniy_kudinov
01.09.2026 18:33Я к аналогичным выводом пришел. Перебираю языки, где корректность логики можно верифицировать средствами системы типов и в этом плане интересен Idris2. При этом выразительность и компактность выражения намерений.
diflux Автор
01.09.2026 18:33Согласен. Idris2 — отличный инструмент для верифицируемого кода, но он требует, чтобы разработчик мыслил на уровне типов.
Зависимые типы — это мощнейший инструмент, и если мы говорим о доказательстве того, что код строго соответствует спецификации, то Idris2 или Coq/Lean вне конкуренции.
Но здесь кроется нюанс, который мы и пытаемся закрыть: Idris2 доказывает корректность реализации, но не спасает от ошибок в самой спецификации. Если бизнес-аналитик или ИИ забыл описать в спецификации обработку ошибки сети или edge-case, Idris просто безупречно скомпилирует эту неполную логику. Он докажет, что код непротиворечив, но система всё равно упадет в продакшене.
Поэтому мы не пытаемся соревноваться с Idris2 в математических доказательствах — это нереально для сложных систем без команды математиков.
Мы делаем прагматичную верификацию на уровне модели. Наш валидатор проверяет не "истинность теоремы", а структурную целостность графа намерений:
Все ли узлы достижимы? (Нет ли мертвого кода)
Покрыты ли все условия? (Нет ли забытыхelse)
Сходятся ли типы данных между узлами? (Не передаем ли мы строку туда, где ждем число)
Нет ли логических тупиков и циклов?Это не "доказательство корректности программы" в академическом смысле. Это детектирование очевидных архитектурных и логических дыр до того, как они превратятся в код.
Idris2 гарантирует, что вы правильно построили стену по чертежу. А Work Graph гарантирует, что на самом чертеже не забыли нарисовать дверь, прежде чем вы вообще начнете класть кирпичи. И то, и другое нужно, но это разные слои ответственности.
evgeniy_kudinov
01.09.2026 18:33Проблема заключается в ограниченности человеческого мозга. Из-за этого он может утонуть в кодогенерации с помощью ЛЛМ, даже для того чтобы понять, что там происходит. Решение этой проблемы пока не найдено, но, возможно, оно будет включать синтез Work Graph с чем-то математическим и верификатором или оракулом.
cane
01.09.2026 18:33Полностью полагаться на систему типов я бы не стал. За счет типов корректность программы можно получить только частично. тип не решит проблемы в случае если функция возвращает (balance + amount) вместо (balance - amount).
Проектирую язык программирования Orthon.
Систему проверка корректности распределяю по уровням. Каждый уровень ловит свой класс ошибок. Это рациональный компромисс.Уровень 1 (система типов) - структурная корректность. Корректно типизированная программа не упадёт с ошибкой типа в рантайме. Нет null. Отсутствие зашито в Option и сужение типов превращает разыменование None в ошибку компиляции. match конструкция обязана покрывать все варианты. Это дёшево и проверяется целиком до запуска.
Уровень 2 (компилятор как анализатор) - корректность владения и мутации. Семантическая модель задаёт инварианты, которые обязана реализовать любая стратегия реализации: у каждого значения ровно один владелец; мутация требует исключительного доступа, чтение может быть общим; видимость не обходится в рантайме. Компилятор проверяет их статически - висячая ссылка или гонка на общем изменяемом состоянии становятся ошибкой сборки.
Уровень 3 (контракты сигнатур методов) - поведенческая корректность. Здесь живёт логика, которую типы не видят: Пример:
fn withdraw(balance: Int, amount: Int) -> Int requires amount > 0 requires amount <= balance ensures result == balance - amount return balance - amountrequires - предусловие (обязанность вызывающего).
ensures - постусловие (гарантия метода).
Где компилятор может доказать, будет ошибка компиляции. Остальное в debug/test-сборках становится проверками - requires как assert на входе, ensures как assert на выходе, - а в runtime пропускается.Уровень 4 (типы с ограничениями) - корректность значений. Такая я же по сути идея:
type Age = Int requires v >= 0 && v <= 150Ограничение объявлено один раз на типе и проверяется на каждой границе, где в тип входит значение. Сигнатура
fn register(age: Age)уже несёт знание о допустимом диапазоне - без проверки в теле.diflux Автор
01.09.2026 18:33Интересный проект. Похоже, вы строите язык, где корректность встроена в конструкцию, а не добавляется сверху.
Есть параллель с WG, но мы действуем в другом порядке.
Work Graph гарантирует: спецификация корректна по структуре до того, как написан код.
Orthon гарантирует: код корректно написан по спецификации.cane
01.09.2026 18:33В Orthon корректность действительно встроена в конструкцию, но гарантировать можно только структурное соответствие, что код согласован со спецификацией, которая заявлена в самом коде. Компилятор здесь и есть статический анализатор, а семантическая модель задаёт инварианты, которые обязана выполнять любая реализация. Проверять поведенческое соответствие замыслу компилятор и не должен.
evgeniy_kudinov
01.09.2026 18:33Похоже на https://en.wikipedia.org/wiki/Dafny
Есть еще https://github.com/viperproject/gobraДумаю, уже назрело с приходом ЛЛМ-генерации, что нужен какой-то DSL или spec ЯП (декларативный), чтобы создавать на типах теорему с выразительностью и без шума для легкого восприятия человеком, и где реализация (пишет ЛЛМ) - это доказательство описной на типах теоремы. Оракулом выступать будет компилятор(верификатор) DSL.
Судя по SDD, из-за неоднозначности человеческого языка и использования недетерминированного генератора (агент + ЛЛМ) существует риск, что в реальности программа будет работать не так, как задумано (возникнут искажения намерений). Даже прочитав все тщательно, но мозг людей физически ограничен для хранения в своем контексте много информации и легко будет упустить что-либо.
Если математически доказывать корректность программы и её логику, можно будет быть уверенным в правильности основной бизнес-логики.
Но пока все формируется и неясно, как оптимально подобрать компромиссы для реализации. Я пока связку idris2 core + go harness рассматриваю (FFI gen), но со временем, конечно, думаю, нащупают схему.
cane
01.09.2026 18:33Спасибо за наводку с Dafny. Оба языка действительно реализуют подход Correct-by-Construction и используют общие ключевые слова
requires/ensures/invariant. Но делают это по разному.
Dafny полагается на математическое доказательство, а Orthon на архитектуру.
для Orthon корректность это не конечная цель, а средство для других целей: комфорта человека и надёжной генерации кода моделями. Правильность достигается не доказательством произвольных свойств, а тем, что недопустимые состояния структурно невозможно выразить (Владение с move-семантикой, неизменяемость по умолчанию, алгебраические типы с исчерпывающимmatch, литеральные типы,Option/Result). Контракты есть, но занимают скромную нишу на втором ярусе инвариантов.
diflux Автор
01.09.2026 18:33Спецификации на типах в классическом стеке кажется утопией. Мы обходим это, вынося верификацию за пределы языка, в собственный слой. А код получает ровно ту типизацию, которую язык поддерживает из коробки.
NecroOasis
01.09.2026 18:33А может просто сделать еще лучше: не срать нейрослопом в продакшин, а использовать для референса, а потом переписать.
diflux Автор
01.09.2026 18:33Согласен, нейрослоп в продакшене — зло. Но переписать руками — это как раз та самая операционная энтропия, от которой мы пытаемся избавиться.
Мы сейчас двигаемся в сторону, когда нейросеть в нашей системе вообще не генерирует код. Она генерирует только формальное описание логики (контракты).
Валидатор математически проверяет граф на полноту, отсутствие тупиков и соответствие типам. Если проверка пройдена, детерминированный компилятор превращает этот граф в чистый, типизированный код.
Нейросеть здесь выступает не как программист, а как переводчик с человеческого языка на строгий протокол. А код уже пишет машина, которая не умеет срать, потому что следует жёстким, верифицируемым правилам. По итогу у нас должен получиться протокол надежности для ИИ.
cane
01.09.2026 18:33используете ли Вы для описания контрактов стандарты, ODCS например?
https://martinfowler.com/articles/making-data-ready-for-agentic-ai.htmldiflux Автор
01.09.2026 18:33У нас уровень выше — формализуем не данные, а логику и намерения.
Мы строим не контракты на данные, а контракты на исполнение правил.
ODCS описывает контракты на данные: их схему, качество, свежесть. Это про то, как данные должны выглядеть, чтобы ИИ мог им доверять.Work Graph описывает контракты на поведение: что система должна делать, какие у этого есть предусловия и постусловия, как проверить результат. Это про то, как ИИ должен действовать, а не только что читать.
Dhwtj
Трассировка требований?
Кажется, милениалы заодно переизобрели (IBM) Rational Requisite Pro , который кажется был заменён на requirements composer (был такой, лет 20 назад не взлетел).
diflux Автор
20 лет назад аналитики вручную связывали требования с кодом. Матрица устаревала быстрее, чем её обновляли. Дорого, скучно, бессмысленно.
Сейчас ИИ генерирует код из формализованных требований. Трассировка создаётся автоматически как побочный продукт. Ноль ручного труда.
Rational RequisitePro требовал дополнительной работы для поддержки трассировки. Work Graph делает трассировку "условно бесплатной" — она возникает сама по себе.
Это как разница между ручным вводом данных в Excel и автоматической синхронизацией через API. Одно и то же по сути, но разная экономика усилий.
Dhwtj
Не только.
Ещё проблема была что связи между требованиями нечёткие, не очевидные. Совершенно неверно считать что требование А противоречит требованию Б. Оно может сочетаться, но повысить стоимость, а может оказаться что требование Б слишком грубое, его надо разбить на С и Д, уменьшить ограничения, поскольку в реальности их и нет, требование Б было слишком грубой моделью.
Ну и так далее. Долго не работал с ним.
Полагаю, вы с этим тоже столкнетесь. Нечёткость, несовершенство заложенной ранее модели мешает её модифицировать. Некий технический долг.