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