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

Модель мышления: не талант, а способ смотреть на правила

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

Классическая работа Saeed Dehnadi и Richard Bornat *The camel has two humps описывает знаменитый «двухгорбый» распределение успехов на первых курсах программирования. Значительная доля студентов — иногда до половины потока — не проходит вводный курс, несмотря на мотивацию, хороших преподавателей и смену языков и методик за десятилетия. Авторы показали, что до изучения синтаксиса Java или Python можно довольно надёжно предсказать, кто «поймёт», а кто будет бороться, с помощью простого теста на последовательность присваиваний — не на знание языка, а на согласованность ментальной модели вычисления.

Что такое «правильная модель мышления» в их смысле

Dehnadi и Bornat опираются на идею mental models (ментальных моделей): человек, рассуждая, строит воображаемое «состояние мира», проверяет в нём гипотезу и ищет контрпримеры Johnson-Laird, Mental Models . В эксперименте «верблюд с двумя горбами» студентам давали короткие фрагменты псевдокода с присваиваниями. Оказалось, что успешные новички последовательно интерпретируют присваивание как правило перезаписи ячейки памяти: «сначала вычисли выражение справа, затем положи результат в переменную слева, старое значение исчезает». Неуспешные часто смешивают модели: где-то видят «равенство», как в уравнении из школьной математики, где-то — «копирование слева направо», где-то отказываются отвечать, потому что «это бессмысленно».

Эта статья – о Pet project, собственных проектах, которыми многие из нас занимаются в свободное время. Поговорим о том, нужны ли такие увлечения архитектору и как Pet project может помочь в работе. Также я расскажу о своих проектах и опыте, который я с их помощью получил. Добро пожаловать под кат!