Как миллениалы переизобрели контрактное программирование для ИИ

[Dhwtj]

Трассировка требований?

Кажется, милениалы заодно переизобрели (IBM) Rational Requisite Pro , который кажется был заменён на requirements composer (был такой, лет 20 назад не взлетел).

[diflux]

20 лет назад аналитики вручную связывали требования с кодом. Матрица устаревала быстрее, чем её обновляли. Дорого, скучно, бессмысленно.

Сейчас ИИ генерирует код из формализованных требований. Трассировка создаётся автоматически как побочный продукт. Ноль ручного труда.

Rational RequisitePro требовал дополнительной работы для поддержки трассировки. Work Graph делает трассировку "условно бесплатной" — она возникает сама по себе.

Это как разница между ручным вводом данных в Excel и автоматической синхронизацией через API. Одно и то же по сути, но разная экономика усилий.

[Politura]

Чего не хватает современным инструментам?

Перестать делать "херак-херак и в продакшен". Натренированные на тоннах индусского кода, когда зп или промоушен видимо зависел от количества строчек кода, а не от его смысла, все эти Опусы зачастую стараются сильно переусложнять код. Правильное слово overengineering, хз как это по-русски сказать. И как вы с этим собираетесь бороться? Работать-то оно работает.

[diflux]

Следующий шаг Work Graph — стать генеративным Low-Code. Overengineering становится просто невозможным: если решение можно собрать из существующих кирпичиков — ИИ обязан использовать их, а не изобретать велосипед.

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

[evgeniy_kudinov]

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

[diflux]

Согласен. Idris2 — отличный инструмент для верифицируемого кода, но он требует, чтобы разработчик мыслил на уровне типов.

Зависимые типы — это мощнейший инструмент, и если мы говорим о доказательстве того, что код строго соответствует спецификации, то Idris2 или Coq/Lean вне конкуренции.

Но здесь кроется нюанс, который мы и пытаемся закрыть: Idris2 доказывает корректность реализации, но не спасает от ошибок в самой спецификации. Если бизнес-аналитик или ИИ забыл описать в спецификации обработку ошибки сети или edge-case, Idris просто безупречно скомпилирует эту неполную логику. Он докажет, что код непротиворечив, но система всё равно упадет в продакшене.

Поэтому мы не пытаемся соревноваться с Idris2 в математических доказательствах — это нереально для сложных систем без команды математиков.

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

Все ли узлы достижимы? (Нет ли мертвого кода)
Покрыты ли все условия? (Нет ли забытых else)
Сходятся ли типы данных между узлами? (Не передаем ли мы строку туда, где ждем число)
Нет ли логических тупиков и циклов?

Это не "доказательство корректности программы" в академическом смысле. Это детектирование очевидных архитектурных и логических дыр до того, как они превратятся в код.

Idris2 гарантирует, что вы правильно построили стену по чертежу. А Work Graph гарантирует, что на самом чертеже не забыли нарисовать дверь, прежде чем вы вообще начнете класть кирпичи. И то, и другое нужно, но это разные слои ответственности.

[cane]

Полностью полагаться на систему типов я бы не стал. За счет типов корректность программы можно получить только частично. тип не решит проблемы в случае если функция возвращает (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) уже несёт знание о допустимом диапазоне - без проверки в теле.

[diflux]

Интересный проект. Похоже, вы строите язык, где корректность встроена в конструкцию, а не добавляется сверху.

Есть параллель с WG, но мы действуем в другом порядке.

Work Graph гарантирует: спецификация корректна по структуре до того, как написан код.
Orthon гарантирует: код корректно написан по спецификации.

[NecroOasis]

А может просто сделать еще лучше: не срать нейрослопом в продакшин, а использовать для референса, а потом переписать.

[diflux]

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

Мы сейчас двигаемся в сторону, когда нейросеть в нашей системе вообще не генерирует код. Она генерирует только формальное описание логики (контракты).

Валидатор математически проверяет граф на полноту, отсутствие тупиков и соответствие типам. Если проверка пройдена, детерминированный компилятор превращает этот граф в чистый, типизированный код.

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