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