28 августа 2026 года в блоге Stack Overflow вышла беседа с Лео де Моура, создателем языка Lean и Senior Principal Applied Scientist в AWS. Для рынка, где все дружно ускоряют верификацию AI-агентов до состояния «потом разберемся», это неприятно трезвый сигнал: если агент пишет, оптимизирует и переписывает код сам, проверять его вывод по старинке уже мало.
В разговоре, о котором сообщает Stack Overflow Blog, де Моура обсуждает сразу три темы: как с помощью Lean доказывать корректность поведения AI-агентов, почему автоматизированное рассуждение не конкурирует с вероятностными моделями, а дополняет их, и как ИИ можно использовать для непрерывной оптимизации кода. Сам по себе набор тезисов не новый, но важен источник: это не маркетинг очередного «умного помощника», а позиция человека, который давно строит инструменты, где слово correctness означает не «вроде работает», а «это можно доказать».
Ключевой объект здесь, конечно, Lean. Это функциональный язык программирования и proof assistant, то есть система, в которой можно не только писать программу, но и формально проверять ее математическую корректность в той же среде. В документации Lean проект описывается как попытка свести программирование и доказательство в одну систему, а сам проект был запущен Леонардо де Моура в 2013 году. Для обычной продуктовой разработки такая постановка долго выглядела слишком академично: формальная верификация ассоциировалась с криптографией, компиляторами, авиацией и другими местами, где ошибка стоит слишком дорого. Но после бума генеративного ИИ логика меняется. Когда код генерируется быстрее, чем команда успевает его ревьюить, интерес к верификации AI-агентов перестает быть хобби для любителей теории типов.
Собственно, на этом и строится главный тезис беседы. Вероятностные модели хороши в поиске вариантов, синтезе кода и работе с нестрогими требованиями, но они по определению не дают гарантий истинности результата. Они угадывают, иногда блестяще, иногда с очень уверенным лицом ошибаются. Автоматизированное рассуждение и proof-системы вроде Lean работают в другой плоскости: не генерируют правдоподобный ответ, а проверяют, следует ли он из формально заданных правил. Для разработчиков это важное разделение. Если LLM помогает написать функцию, тесты еще могут поймать часть проблем. Но если агент начинает сам рефакторить систему, менять инварианты, трогать безопасность, конкурентность или бизнес-логику, цена ложноположительной уверенности резко растет. Здесь «модель была очень уверена» уже не аргумент.
На практике это подводит отрасль к довольно прозаичному сценарию. ИИ выступает как быстрый генератор гипотез: предлагает код, переписывает участки, ищет упрощения, оптимизирует реализацию. А поверх этого нужен слой строгой проверки, который подтверждает, что после всех улучшений система сохраняет нужные свойства. Не просто проходит тестовый набор, а действительно не нарушает заранее описанные ограничения. Для CTO и техлидов это звучит как лишний уровень сложности, и формально так и есть. Но альтернатива еще дороже: бесконечно раздувать ревью, тестирование и постфактум-отладку в надежде, что генеративная скорость как-нибудь сама приведет к качеству.
Отдельно интересна тема continuous code optimization, которую затронули в разговоре. Рынок давно продает идею ИИ как автора кода, но следующий логичный этап не написание с нуля, а постоянная машинная доработка уже существующей кодовой базы. Агент видит узкие места, пробует более эффективную реализацию, сокращает дублирование, меняет структуры данных, переписывает функции. Проблема в том, что такие улучшения легко превращаются в очень дорогие регрессии. Если же рядом есть формальная спецификация и инструмент, который может проверить сохранение инвариантов, оптимизация становится менее похожей на азартную игру. Не безопасной по умолчанию, но хотя бы инженерно контролируемой.
Для русскоязычной IT-аудитории тут есть еще один практический вывод. На локальном рынке разговор об ИИ в разработке пока часто застревает между двумя крайностями: «все заменит» и «это просто автодополнение». Беседа Stack Overflow интересна тем, что предлагает более взрослую рамку. Не спорить, заменит ли модель программиста, а разложить стек обязанностей: где ИИ полезен как вероятностный генератор, а где нужен механизм формального доверия. Для разработчиков это означает рост спроса на навыки, которые еще недавно считались нишевыми: спецификации, инварианты, типовые системы, статический анализ, reasoning-инструменты. Для бизнеса вывод проще: чем активнее компания встраивает агентов в разработку, тем важнее ей не только скорость генерации, но и доказуемая корректность хотя бы на критичных участках.
Пока Lean и подобные системы не станут массовым стандартом во всем софте, и никто всерьез не обещает такого завтра. Но тренд уже читается довольно четко: индустрия устала делать вид, что больше AI-кода автоматически означает больше инженерной эффективности. Следующий раунд конкуренции, похоже, будет не за самого разговорчивого агента, а за того, чьи изменения можно проверить не по настроению ревьюера, а по формальным правилам.