Верификация программного обеспечения в эпоху искусственного интеллекта

Перевод доклада Бертрана Мейера (Eiffel Software, Recognyze AI) с ACM Technology Talk, 7 мая 2026 г. Отредактированная стенограмма и раздаточный материал. Более структурированное изложение — в статье «От вероятного к доказуемому» (Communications of the ACM, июнь 2026) и в готовящейся книге «Понимание искусственного интеллекта: триумф эмпиризма».

От переводчика. Это перевод митап-доклада Бертрана Мейера — создателя языка Eiffel и концепции «проектирования по контракту», автора классического «Object-Oriented Software Construction». Доклад показался мне прямым продолжением [моей прошлой статьи про машину Тьюринга и ментальные модели разработчика](https://habr.com/ru/articles/1041868/): там речь шла о том, какая модель мышления нужна программисту, здесь — о том, почему именно эта модель становится критичной, когда код за нас пишет ИИ. В нескольких местах я добавил блоки-вставки со своими размышлениями — они помечены значком 💭 и отделены от авторского текста.

Аннотация

Генеративный ИИ возродил давнее обещание, что нам больше не придётся писать программы — что достаточно будет лишь сформулировать требования, а машина сделает остальное. В этой статье данное обещание рассматривается через призму программной инженерии и, в особенности, верификации. Утверждается, что хотя современный ИИ действительно меняет способ создания программ, кодирование составляет лишь малую долю программной инженерии; что трудные части — требования, архитектура и прежде всего проверка и верификация (V&V) — остаются трудными; и что определяющий вид отказа ИИ, галлюцинация, делает гарантии корректности более, а не менее важными. Мы рассматриваем измеренные свидетельства инцидентов, связанных с ИИ, напоминаем, почему «почти корректные» компоненты складываются в ненадёжные системы, и описываем эксперимент по созданию формально верифицированной системы управления конференциями с помощью ИИ-ассистента и среды AutoProof для языка Eiffel. Из этого опыта мы выводим итеративный процесс — специфицируй понемногу, реализуй понемногу, пытайся верифицировать, исправляй — и взгляд на инструментальную цепочку как на федерацию взаимодействующих ИИ-агентов. Вывод осторожно оптимистичен: для повседневных разработок ИИ — это нивелирующая технология, способная во многом автоматизировать работу; для деловых и критических разработок это усиливающая технология, и уроки программной инженерии применимы как никогда.

1. Раскрывая карты

Начну с вывода, представленного в виде картинки. Будущее создания программ — это не единственный оракул, который проглатывает пожелание и выдаёт готовую систему. Это экосистема специализированных агентов — агент требований, агент архитектуры, агент контрактов, агент кодирования, агенты для тестирования, генерации тестов, доказательства и развёртывания — взаимодействующих вокруг инженера-человека (рис. 1). Человек не исчезает; человек направляет, разрешает споры и несёт ответственность. Всё дальнейшее объясняет, почему я пришёл к этой картине и почему агенты доказательства и контрактов — не декоративные украшения, а несущие конструкции.

2. Утверждение и его история

Вирусный твит годичной давности прекрасно передал настроение: с сегодняшними моделями, гласил аргумент, вы больше не пишете код — вы описываете функцию на обычном английском, и ассистент пишет, запускает, копирует, вставляет и выпускает её; если возникает ошибка, вы вставляете её обратно и даёте модели всё исправить; «в основном работает». Лозунг сводится к одной фразе: просто сформулируй, что тебе нужно, и ИИ сделает за тебя остальное.

«Появился новый язык программирования. Он называется английским». — Дженсен Хуанг, CEO NVIDIA, 2024

CEO компании NVIDIA был самым цитируемым сторонником этой идеи. В 2024: «Наша задача — создать вычислительную технологию, при которой никому не придётся программировать… теперь каждый в мире — программист». В январе 2026: «Все думали, что программирование — это венец интеллектуальных профессий. Посмотрите, что ИИ решает в первую очередь». В марте 2026: «Я хочу, чтобы наши инженеры тратили ровно ноль процентов времени на написание кода… Я хочу, чтобы они были директорами ИИ-агентов».

Мы это уже слышали. Обещание, что программирование растворится в простой спецификации, повторяется раз в десятилетие: автоматическое программирование в 1960-х; «конец программистов» в 1970-х; языки пятого поколения и CASE-средства в 1980-х; компонентная разработка в 1990-х; модельно-ориентированные подходы в 2000-х; low-code и no-code в 2010-х. Каждая волна действительно повышала уровень абстракции — и каждый раз программист выживал, работая на новом уровне. Честный вопрос не «случится ли это?», а «*в этот раз иначе?*». Два наблюдения охлаждают аналогию. Во-первых, программисты в прежних высокоуровневых подходах, как правило, не смотрели на сгенерированный код. Во-вторых, программисты, использующие генеративный ИИ сегодня, всё ещё должны уметь смотреть на него — и судить о нём.

3. Два вида прорыва: тип L и тип E

Чтобы рассуждать об эффекте ИИ, нужно различение. Одни технологии нивелируют навык (тип L): они сглаживают разрыв между новичком и экспертом. AutoCAD, GPS-навигация, фотоаппараты «навёл и снял» и программы для подготовки налоговых деклараций позволяют почти любому достичь компетентного результата. Другие технологии усиливают навык (тип E): они поднимают потолок для тех, кто уже владеет мастерством. Печатный станок, терминалы Bloomberg, профессиональное фотооборудование, объектно-ориентированное программирование и GPU делают экспертов значительно сильнее, мало что давая неподготовленным.

1. Тип L — революционный навык

   1. AutoCAD;

   2. GPS-навигация;

   3. фотоаппараты «навёл и снял»;

   4. программы для налоговых деклараций

2. Тип E — усиливающие навык

   1. Печатный станок;

   2. терминалы Bloomberg;

   3. профессиональное фотооборудование;

   4. объектно-ориентированное программирование; GPU

ИИ в программировании — это и то, и другое, в зависимости от задачи; к этому мы вернёмся в заключении. Категория, к которой относится конкретная разработка, во многом определяет, насколько мы должны доверять автоматизации.

💭 Размышление переводчика: почему ООП оказалось «усиливающим», а не «нивелирующим» Обратите внимание на деталь, которую Мейер роняет почти мимоходом: объектно-ориентированное программирование он относит к технологиям типа E — тем, что усиливают уже умелого, но мало что дают неподготовленному. Это ровно та мысль, к которой я подводил в [прошлой статье](https://habr.com/ru/articles/1041868/): инструмент не создаёт ментальную модель за вас, он лишь даёт ей рычаг.

ООП и паттерны проектирования сами по себе не делают код лучше — это видно по любому проекту, где AbstractSingletonProxyFactoryBean плодятся без понимания, зачем. Но тому, кто уже мыслит программу как систему взаимодействующих состояний, ООП даёт словарь, чтобы эти состояния называть и изолировать, а паттерны — каталог проверенных способов управлять их сложностью. Паттерн — это не рецепт «скопировать и вставить», а упражнение на правильную модель мышления: он заставляет спросить «кто здесь несёт ответственность за состояние? где граница? что меняется, а что остаётся инвариантным?». Именно эти вопросы, а не имена паттернов, и есть ценность.

4. B.A.D.: дисциплина избегания вздора

Предлагаю самостоятельно догадаться что скрывается за абревиатурой BAD

Споры об ИИ тонут в анекдотах. Чтобы оставаться честным, я стараюсь следовать дисциплине, которую называю B.A.D. Её правила: основывай выводы — особенно отрицательные — на новейших профессиональных версиях инструментов (многое существенно изменилось к 2026 году, и приговор, вынесенный старой бесплатной модели, ничего не стоит); основывай выводы на измеренных, а не анекдотических свидетельствах; и отличай ранние сбои от устойчивых, структурных свойств.

Дисциплина режет в обе стороны, поэтому её следует применять и к скептикам. Вспомните первоначальный обзор первого iPhone от CNET (30 июня 2007), который хвалил дисплей, но предупреждал о нестабильном качестве связи, медленной сети передачи данных и скудной памяти и в целом был сдержан. Некоторые «сбои» были реальными; пренебрежительный тон — нет. Урок в том, чтобы отделять временные дефекты от структурных пределов — в любом направлении.

5. О чём идёт речь? Шкала A/B/C

«Программное обеспечение» — не нечто единое. Полезная классификация (из заметки в блоге 2014 года) сортирует разработки по их критичности на три класса: A — критические (Acute), где отказ катастрофичен (авионика, медицинские приборы, финансовые ядра); B — деловые (Business), обширная середина корпоративного и продуктового ПО, где отказ обходится дорого; и C — повседневные (Casual), скрипты и одноразовые инструменты, где дефект — лишь досада. Уместный уровень доверия к ИИ — и уместный процесс — резко различается для этих трёх классов. Большинство восторженных заявлений верны, в лучшем случае, для класса C.

6. С другой стороны: измеренные свидетельства

Два факта неловко соседствуют с риторикой «кодирование решено». Первый: те самые компании, что провозглашают конец программирования, активно нанимают старших инженеров-программистов — на роли Python, сетевые, DevOps, платформенные, опубликованные «вчера». Второй, более показательный — растущий список отказов, связанных с ИИ, собранных в духе B.A.D. из измеренных источников:

• Сбой у крупного ритейлера в марте 2026 — порядка 120 000 потерянных заказов и 1,6 млн ошибок сайта — отнесённый к «новому использованию генеративного ИИ, для которого лучшие практики и меры предосторожности ещё не вполне устоялись», после чего последовал 90-дневный «сброс безопасности кода».

• Университетское отслеживание, приписывающее десятки новых CVE за один месяц напрямую ИИ-инструментам кодирования; а также вывод, что около 20% сгенерированного ИИ кода ссылается на пакеты, которых не существует.

• Многомиллионный эксплойт DeFi-протокола, в уязвимом коде которого ИИ-ассистент значился соавтором.

• Отраслевой отчёт, обнаруживший, что 43% изменений кода, сгенерированного ИИ, потребовали ручной отладки даже после прохождения контроля качества; ни один респондент не смог верифицировать предложенное ИИ исправление за один цикл повторного развёртывания, а 88% потребовалось два или три.

• Криминалистический аудит, сообщивший, что 92% кодовых баз, сгенерированных ИИ, содержали хотя бы одну критическую уязвимость, в среднем 8,3 эксплуатируемых находки на приложение.

Ничто из этого не означает, что ИИ бесполезен. Это означает, что трудная задача не решена — лишь перемещена.

7. Так что же такое программная инженерия?

Предположим, кодирование действительно мог бы взять на себя ИИ. И что тогда? Программная инженерия гораздо шире кодирования. Она включает инженерию требований; архитектуру и проектирование; кодирование (лишь около 10–20% усилий); проверку и верификацию — тестирование и отладку; сопровождение, расширение и повторное использование; а также управление проектом, измерения и улучшение процесса. Автоматизация тех 10–20%, что составляют кодирование, даже полная, оставляет нетронутым большинство дисциплины — и, возможно, делает остальные части труднее, ведь теперь они должны ещё и контролировать плодовитого, самоуверенного и порой выдумывающего соавтора.

8. «Просто» сформулируй, что тебе нужно

Всё обещание ИИ держится на одном невинном слове: просто. «Просто сформулируй, что тебе нужно». Но точно, полно и непротиворечиво сформулировать, что система должна делать, — и есть инженерия требований, одна из самых трудных частей программной инженерии, предмет целого «Справочника по требованиям и бизнес-анализу» (рис. 2). Естественный язык неоднозначен; заинтересованные стороны расходятся во мнениях; самые тяжёлые дефекты — это дефекты требований, а не кода. Передача пожелания ИИ не устраняет эту трудность; она лишь прячет её — а ИИ, самоуверенно заполняющий пробелы правдоподобными догадками, — именно неподходящий инструмент для работы, требующей дисциплинированного сомнения.

💭 Размышление переводчика: «просто сформулируй» упирается в ту же стену, что и x = x + 1

Когда Мейер говорит, что «просто сформулировать, что нужно» — это и есть самая трудная часть, я слышу эхо того, о чём писал раньше. Исследование Дехнади и Борната показало: половина новичков не может стабильно удержать в голове, что присваивание x = x + 1 — это перезапись ячейки памяти, а не математическое равенство (которое было бы абсурдом). Барьер не в синтаксисе — он в модели.

Сформулировать требование точно — это та же работа, только на более высоком уровне абстракции. Чтобы написать корректную спецификацию, нужно мысленно прогонять систему по состояниям: что истинно до операции, что должно стать истинным после, что обязано сохраняться всегда. Это ровно мышление «изменяющихся состояний», а не «абстрактной истины». ИИ-ассистент не обладает этой моделью — он интерполирует правдоподобный текст. Поэтому ответственность за то, чтобы спецификация описывала настоящую машину состояний, а не красивую сказку о ней, остаётся на человеке. Машину Тьюринга в голове пока никто не отменял.

9. Галлюцинации

Определяющее свойство больших языковых моделей и их определяющая опасность для ПО — галлюцинация: гладкий, уверенный вывод, который попросту неверен (офорт Домье, рис. 3, — удачная эмблема). В тексте галлюцинация — конфуз; в коде это несуществующая зависимость, неправильно использованный API, тихо нарушенный инвариант. Хуже то, что мы называем петлями галлюцинаций: вы сообщаете об ошибке, модель «исправляет» её, вводя другую, вы сообщаете о ней, и так далее — диалог сходится к уверенности, а не к корректности. Наша работа «Помогают ли ИИ-модели создавать верифицированные исправления ошибок?» (выйдет на VERIFAI-2026; arXiv:2507.15822) рассматривает именно этот вопрос.

💭 Размышление переводчика: галлюцинация ловится только моделью в голове

Петля галлюцинаций — это очень узнаваемый сценарий «вайб-кодинга»: модель уверенно правит код, диалог сходится к убедительности, а не к корректности. Вырваться из этой петли может только тот, у кого есть независимый источник истины — собственное понимание того, что код обязан делать.

Именно здесь, на мой взгляд, окупается дисциплина, которую воспитывают ООП и паттерны. Инвариант класса, чёткое разделение ответственности, понимание, кто владеет состоянием, — это и есть тот внутренний эталон, с которым можно сверить «уверенный» ответ ИИ. Разработчик без этой модели обречён верить ассистенту на слово; разработчик с моделью видит «тихо нарушенный инвариант» раньше, чем компилятор. Я писал об этом так: даже если ИИ генерирует синтаксически корректный код, ответственность за вычислительную корректность остаётся за человеком. Мейер говорит ровно то же — только с математикой композиции в руках (см. §11).

10. Современный ИИ: триумф эмпиризма

Чтобы понять, почему галлюцинация присуща ИИ, а не случайна, вспомним, что это за системы. Современный ИИ основан на вероятности и статистике: машинное обучение, нейронные сети, архитектура трансформеров — «стохастические попугаи». Его руководящий принцип: «не проектируй то, чему можно научиться», триумф эмпиризма, ставший возможным благодаря прогрессу в аппаратуре (GPU) и Сети как огромному обучающему корпусу, охватывающему большую часть человеческих знаний. Для кода этот корпус огромен: порядка 60 млн публичных репозиториев GitHub (оценочно 100–500 млрд строк), десятки миллионов постов Stack Overflow плюс книги и энциклопедические статьи с кодом. Система, интерполирующая по такому корпусу, чрезвычайно полезна — и конституционально неспособна что-либо гарантировать. Этот разрыв и есть весь предмет доклада.

11. От вероятного к доказуемому

Почему «вероятно корректно» недостаточно? Потому что ПО составляется из частей. В проекте ESPRIT 1980-х Хоар и Рэнделл занимались «Проектированием доказуемо безопасной операционной системы» (рис. 5), исходя из того, что для критических систем правдоподобие — не гарантия. Простой расчёт, по замечанию Дейкстры в «Структурном программировании» (1970), показывает, почему (рис. 4). Пусть каждый модуль независимо корректен с вероятностью 99,9%. Вероятность того, что составленная из них система корректна, равна 0,999 в степени n; для 1000 модулей — около 37%; для 5000 модулей — менее 1%. «Почти корректные» компоненты перемножаются в системы, которые почти наверняка некорректны. Это математическое сердце аргумента: ИИ даёт нам вероятный код дёшево, но инженерия любого значения требует перехода от вероятного к доказуемому (Communications of the ACM, июнь 2026; препринт arXiv:2511.23159).

💭 Размышление переводчика: два темперамента — это математик и программист из прошлой статьи

«0,999 в степени n» — это, пожалуй, самый мощный график во всём докладе. И он же объясняет, почему я в прошлый раз так настаивал на различении двух способов мышления. Статистическое мышление (ИИ) оптимизирует средний случай и терпимо к ошибкам; дедуктивное (инженерное) одержимо худшим случаем и нетерпимо к ним. Это та же оппозиция, что между мышлением «абстрактной истины» математика и мышлением «изменяющихся состояний» программиста — только перенесённая на уровень целых культур разработки.

Мораль для практика проста: нельзя строить надёжную систему из «вероятно корректных» кирпичей, полагаясь на статистику. Нужен момент, где вероятность превращается в доказательство — пусть локальное, пусть в одном инварианте. И способность мыслить в категориях инвариантов и контрактов воспитывается заранее, на учебных задачах и паттернах, а не в ночь перед релизом критической системы.

12. Брак двух культур

ИИ и программная инженерия — по темпераменту странная пара (рис. 6): одна статистическая, терпимая к ошибкам, оптимизирующая средний случай; другая дедуктивная, нетерпимая к ошибкам, одержимая худшим случаем. У разработки ПО всегда было два этих лица — вдохновлённое и дисциплинированное (картина Каульбаха «Фауст и Мефистофель» служила эмблемой этой пары). Интересный вопрос — может ли брак быть счастливым. Я буду утверждать, что может — но лишь если каждый партнёр сохраняет свою роль.

## 13. Процесс: V-модель и реальность

Классическая V-модель (рис. 7) раскладывает разработку как спуск через требования, системный анализ, проектирование и проектирование модулей к кодированию, а затем симметричный подъём через модульное, интеграционное, системное и приёмочное тестирование, где каждая фаза верификации зеркалит фазу спецификации. Это полезная педагогическая идеализация. Честная картина запутаннее (рис. 8): реальная разработка — заросли вложенных, повторяющихся мини-V, итерация на всех уровнях. Любая реалистичная роль ИИ должна вписываться именно в эту реальность, а не в учебную схему.

14. Что формальные методы (во многом) упустили

Если верификация — ответ, почему формальные методы ещё не победили? Блестящие техники — среди них метод B — негласно предполагают, что требования известны. Замечательная миниатюра: попросите формальный набор инструментов «вычислить 8-е число Фибоначчи» и понаблюдайте, сколько скрытой спецификации таит эта невинная фраза. Классическая практика формальных методов также во многом игнорировала объектно-ориентированное программирование, гибкие методологии, DevOps, ценность тестов — особенно неуспешных — и, главное, саму трудность правильного составления спецификации. Путь вперёд должен впитать эти уроки, а не воскрешать мечту формалиста о спецификации, ниспосланной целиком свыше.

15. Контракты и доказательство: Eiffel и AutoProof

Мостом между спецификацией и кодом в моей работе служит проектирование по контракту: предусловия, постусловия и инварианты класса, записанные внутри текста программы (рис. 9). Контракты — не комментарии; это исполняемые, проверяемые спецификации, используемые для тестирования, генерации тестов, отладки, сопровождения и управления проектом. Это именно тот артефакт, который ИИ-ассистент следует заставлять производить и соблюдать.

💭 Размышление переводчика: контракт — это паттерн мышления, а не фича языка

Вот мы и дошли до сердцевины — и до прямого ответа на вопрос, ради которого я затевал эти вставки. Мейер показывает «проектирование по контракту» как технологию Eiffel. Но require/ensure/invariant — это не про синтаксис конкретного языка, это про модель мышления, которую можно (и нужно) носить с собой в любой язык: Python, Java, Go, TypeScript.

Предусловие — это вопрос «при каких состояниях входа я вообще имею право работать?». Постусловие — «что я гарантирую на выходе?». Инвариант — «что обязано быть истинным всегда, между вызовами?». Тот, кто привык думать контрактами, естественно приходит и к паттернам: паттерн — это закристаллизованный ответ на повторяющийся вопрос «как распределить эти гарантии между объектами, не разрушив их инварианты?».

Поэтому связь, на которой я настаиваю, такая: изучение ООП и паттернов — это не зубрёжка каталога GoF, это тренажёр для той самой машины состояний в голове, о которой шла речь в прошлой статье. Контракты делают эту тренировку явной и проверяемой. А в эпоху ИИ именно человек с натренированным «контрактным» мышлением способен заставить ассистента производить не просто правдоподобный, а проверяемый код — и отличить одно от другого.

Поверх контрактов располагается AutoProof (рис. 10), авто-активная среда доказательства: классы Eiffel с контрактами плюс математическая библиотека моделей (MML) для спецификации транслируются в промежуточный верификатор Boogie и разрешаются SMT-решателем. Результат — не «вероятно», а доказано — либо явный, локализованный отказ.

Существенно, что даже неуспешное доказательство продуктивно. Когда AutoProof не может установить постусловие или инвариант, неудавшееся условие верификации прямо указывает на свидетеля — и этого свидетеля можно превратить в полезный тест (рис. 11; ICTSS 2023). Доказательство и тестирование — союзники, а не соперники.

16. На пути к процессу

Сложите части вместе — и возникает процесс, который не является ни грандиозным спуском формалиста, ни свободным падением «вайб-кодинга». Его цикл состоит из четырёх шагов (рис. 12): специфицируй понемногу, реализуй понемногу, пытайся верифицировать и исправляй — затем повторяй. Спецификация и реализация питают друг друга; верификация непрерывно применяется к небольшим приращениям; отказы возвращают к шагу исправления, который может затронуть спецификацию, код или и то, и другое. ИИ ускоряет каждый блок; верификация держит каждый блок честным.

17. Первая вылазка

Чтобы проверить идею, мы провели эксперимент (с Ли Хуаном): мог бы ИИ-ассистент помочь построить небольшую, но полностью, формально верифицированную систему? Задание, данное модели, было намеренно строгим (рис. 13): система управления конференциями — «мини-EasyChair» — написанная на Eiffel и полностью формально доказанная, причём ассистент производит и спецификацию (контракты Eiffel), и код, действуя шаг за шагом, а явная цель — исследовать процесс разработки верифицированного ПО, а не выпустить продукт.

Хорошее

Ассистент был по-настоящему продуктивен на уровне артефактов: он сгенерировал код, предложенную архитектуру, план проекта и — что впечатляет — чистый, ориентированный на верификацию глоссарий предметной области (рис. 14), назвав действующих лиц и роли (автор, рецензент, председатель, член программного комитета), артефакты (статья, версия, рецензия, назначение, решение) и отношения и конфликты между ними. Хорошо назвать предметную область — половина работы по требованиям, и здесь машина помогла.

Удовлетворительное

Предложенная общая схема (рис. 15) была разумной: бережливый, дружественный к верификации процесс — однопоточное детерминированное ядро, абстрагированный ввод-вывод за интерфейсами, призрачное состояние и модельные атрибуты на основе MML, чистые процедуры, минимальный начальный охват и пошаговые поставки, завершающиеся полностью контрактными, дружественными к AutoProof реализациями. Это был правдоподобный план — какой мог бы набросать компетентный инженер, — но план не есть доказательство.

Плохое

Затем вмешалась реальность. Сгенерированный код содержал многочисленные ошибки. Элементарные правила не соблюдались — код, который всегда должен компилироваться, иногда не компилировался. И получить доказуемый код оказалось по-настоящему трудно: ассистент утверждал корректность, которую не установил, и тяготел к описанным ранее петлям галлюцинаций. После многих итераций цикла «специфицируй/реализуй/верифицируй/исправляй» мы всё же достигли настоящих доказательств — AutoProof подтвердил процедуры как верифицированные (рис. 16). Но не всё: некоторые свойства сопротивлялись, и инвариант доказать не удалось (рис. 17), обнажив реальный разрыв между тем, что делал код, и тем, чего требовала спецификация. Этот разрыв — видимый только при попытке доказательства — и есть ценность верификации.

18. ИИ-агенты в поддержку процесса

Эксперимент подтверждает исходную картину (рис. 1). Ни одна модель не делает всё; каждый шаг цикла «специфицируй/реализуй/верифицируй/исправляй» естественно обслуживается выделенным агентом — требований, архитектуры, контрактов, кодирования, тестирования, генерации тестов, доказательства и развёртывания — с инженером-человеком в центре, разрешающим споры между ними. Агент доказательства — это то, что превращает уверенные вероятности остальных в нечто, за что инженер может поручиться.

19. Итоги

• Поддержка программной инженерии со стороны ИИ пришла надолго, и разработку класса C («повседневную») можно по существу автоматизировать.

• Для классов A (критические) и B (деловые) ИИ пока не готов к полному, автономному процессу программной инженерии.

• Существует реальный конфликт культур между ИИ (статистическим) и ПИ (дедуктивной); галлюцинации остаются крупной, структурной проблемой.

• Единственный надёжный путь к гарантиям — формальная верификация; «почти корректно» не складывается.

• Нам нужен ясный, итеративный процесс — реальная разработка ПО итеративна, — и мы лишь в самом начале.

20. Индивидуальные стратегии

Для практика вторжение ИИ — в терминах тип-L/тип-E из §3 — это и то, и другое: нивелирующее для работ класса C и усиливающее для остальных. Перспективы низкоквалифицированного аутсорсинга неясны; перспективы для способных компаний вернуть себе владение своим ПО — превосходны. Конкретно: каждый инженер-программист должен освоить современный ИИ; вы остаётесь ответственным за код, кто бы — или что бы — его ни набрал; качество решающе, особенно корректность, надёжность, расширяемость, повторная используемость и сопровождаемость; и уроки программной инженерии применимы как никогда.

💭 Размышление переводчика: «вы остаётесь ответственным за код» — это и был мой главный тезис

Если выносить из доклада одну фразу, я бы взял эту: вы остаётесь ответственным за код, кто бы — или что бы — его ни набрал. Ровно этим я заканчивал [прошлую статью](https://habr.com/ru/articles/1041868/). ИИ сместил границу того, что значит «писать код», но не сместил границу ответственности.

И отсюда — практический вывод для тех, кто только входит в профессию в 2026-м. Соблазн «вайб-кодить», не разбираясь в основах, велик как никогда. Но рынок, как замечает Мейер цифрами найма, расходится с риторикой: для классов A и B по-прежнему нужны люди, умеющие судить о коде. А способность судить вырастает из фундамента — из понимания, что программа есть машина состояний (машина Тьюринга в пределе), из дисциплины ООП и паттернов, из привычки мыслить контрактами и инвариантами. ИИ — это рычаг типа E: он многократно усилит того, у кого этот фундамент есть, и мало чем поможет тому, у кого его нет. Поэтому учить основы стоит не вопреки эпохе ИИ, а именно ради неё.

21. Счастливый брак?

Итак — может ли брак ИИ и программной инженерии быть счастливым (рис. 18)? Мой ответ — осторожное «да». Пусть ИИ делает то, что хорошо удаётся статистике: порождает, предлагает, набрасывает, ускоряет. Пусть верификация делает то, что хорошо удаётся дедукции: гарантирует. Пусть человек остаётся ответственным и в контуре управления. Призрак ИИ-кодирования и его подлинная привлекательность — два взгляда на одно и то же; дисциплина, что примиряет их, — как и всегда — программная инженерия, нужная теперь как никогда.

Литература

1. B. Meyer. From Probable to Provable. Communications of the ACM, июнь 2026. Препринт: arXiv:2511.23159; doi.org/10.1145/3773295 (готовится).

2. B. Meyer. Understanding Artificial Intelligence: The Triumph of Empiricism. Готовящаяся книга, июнь/июль 2026.

3. L. Huang, I. Mustafin, M. Piccioni, A. Schena, R. Weber, B. Meyer. Do AI Models Help Produce Verified Bug Fixes? Выйдет на VERIFAI-2026, Springer LNCS. arXiv:2507.15822.

4. B. Meyer. Handbook of Requirements and Business Analysis. Springer, 2022. se.ethz.ch/requirements/

5. E. W. Dijkstra, O.-J. Dahl, C. A. R. Hoare. Structured Programming. Academic Press, 1970.

6. C. A. R. Hoare, B. Randell и др. Design of a Provably Secure Operating System. Проект ESPRIT, 1980-е.

7. AutoProof: авто-активный верификатор для Eiffel. autoproof.org

8. О неуспешных доказательствах, дающих полезные тесты. ICTSS 2023 (также SN Computer Science).

9. Тесты и доказательства. arXiv:2601.16239.

10. B. Meyer и др. Agile! agile.ethz.ch/ — и вводный учебник по программированию, touch.ethz.ch.

11. Eiffel и проектирование по контракту. eiffel.com

Перевод и комментарии: Дмитрий Дзюба (dvdemon). Оригинал доклада — ACM Technology Talk, 7 мая 2026 г.