Все пишут про вайбкодинг, кто то даже восхищается, заходя в условный дипсик или чатгпт. Это же лучшая возможность почувствовать себя программистом без понимания, что такое паттерны объектно-ориентированного программирования, функциональный, императивный или декларативный стиль разработки. Но всё ли так радужно или наоборот грустно? И так, что же такое антивайб.

Лучше объяснить на пальцах. Вот свежий пример, как антивайб выглядит вживую. PostgreSQL 19 не вышел в сентябре, хотя последние пять лет мажорные версии выходили как часы. Snowflake написали, что виноват ИИ. Мол, находит очень много сложных багов, только и успевай их чинить. Томаш Вондра, коммиттер Postgres, разобрал все откаты и показал, что дело не в этом. Откаты связаны с тем, что обычное ревью людьми не случилось или случилось очень поздно. А всё потому, что число отчётов об уязвимостях выросло с 5 до 44 за год, большинство найдены с помощью ИИ, и опытные разработчики весь цикл разбирали их вместо того, чтобы делать ревью!

Вондра называет это инверсией ИИ. Раньше, чтобы прислать патч или отчёт, нужно было разобраться в коде и сформулировать мысль. Это само собой ограничивало поток. Теперь правдоподобный патч или отчёт генерируется почти даром, а проверять и кодить всё равно должен человек, причём самый опытный и самый занятый.

Многие хорошие программисты пишут отличные решения, но совсем не интересуются компьютерными науками. А вот оказывается есть теорема, которую из-за хайпа на ИИ-агентов почти не вспоминают. Хотя именно она объясняет, почему вайбкодинг в большой компании заканчивается плохо. Теорема Райса, 1953 год.

В кейсе Постгреса, думаю, что ровно теорема Райса в действии. Написать стало дёшево, автоматически проверить также почти бесплатно, а вот по-человечески проверить по-прежнему дорого, и очередь на проверку растёт у тех, кто единственный умеет проверять. В Postgres это закончилось волной откатов в сентябре.

В энтерпрайзе это закончится тем же, только вот об этом не будут писать публично.

Звучит кстати та самая теорема Райса примерно так. Нельзя написать программу, которая для любой другой программы точно ответит на содержательный вопрос о её поведении. Например, зациклится или нет, вернёт ли когда-нибудь отрицательный остаток, делает ли то, что написано в задании. Для любого проверяльщика найдётся программа, на которой он соврёт или зависнет. Это не про слабость компьютеров. Это математика, как теорема Пифагора. Как говорят, пифагоровы штаны во все стороны равны и ничего тут не попишешь )

Казалось бы, и что? А то, что из неё следует вещь, которую каждый айтишник знает на своей шкуре, но правда не связывает ни с теоремой и ни с супер интеллектуальными технологиями. Раз общего проверяльщика нет, код проверяет человек! Читает глазами. Тесты помогают, типы помогают, но они проверяют кусочки, а целиком смысл восстанавливает человек. И человек читает с конечной скоростью. Количество людей, которые способны не только читать код, но и понимать, вообще-то тоже конечно.

Вот отсюда и берётся предел размера системы. Не из теоремы напрямую, а из её следствия. Система может расти, пока люди успевают понимать, что в ней написано. Как только код пишется быстрее, чем читается, начинает копиться непонятое. Это называется легаси. Раньше на это уходило лет двадцать.

Теперь появились ИИ-агенты. Все менеджеры думают уже об оптимизации и полны оптимизма в предвкушении снижения затрат. Ведь ИИ пишет в десять или сто раз быстрее человека, только успевай токены или электричество оплачивать. Но вот читают смыслы по-прежнему люди. Скорость написания выросла, скорость проверки не поспевает. То, что копилось двадцать лет, теперь копится за год. Это не прогноз, это уже видно в проектах, где код пишут агенты, а ревью делают по диагонали теми же ИИ-агентами. Код стареет, не успев родиться.

Но читатель, который в теме, должен сказать. Так можно это починить харнесом, который ограничит работу ИИ-агентов. Ну там линтеры, типы, автотесты, контракты, фаззинг, вторая реализация и все дела. Отчасти да. Но важно понять, что именно он делает. Теорема Райса запрещает общий проверяльщик. Частные она не запрещает. Типы проверяют одно свойство, тесты другое, контракты третье. Харнес работает ровно настолько, насколько важные свойства удалось выразить такими частными проверками. Всё, что не выразили, по-прежнему читает человек. Для обычного кода это большая часть. Так что харнес не отменяет предел, он его отодвигает. И его будут нарушать, когда сроки горят и ещё что-то подгорает.

А теперь возможно есть таблетка. Теорема Райса действует для языков, на которых можно написать что угодно. Их называют тьюринг-полными. Python, Java, JavaScript, Clojure, всё, на чём пишут. Но есть языки, на которых написать что угодно нельзя. На них нельзя написать бесконечный цикл. Нельзя обратиться в сеть. Нельзя сгенерировать случайное число. Зато для любой программы на таком языке можно заранее вычислить, что она сделает.

Для такого языка Райс не действует. Не потому что теорему обошли. Потому что она про другой класс языков. Например, можно использовать декларативный диалект Datalog, маленький язык правил. В нём есть проверки, права, вычисления, реакции. Но нет циклов до бесконечности и нет обращений наружу. Правило либо корректно, либо нет, и машина это решает за конечное время. Не человек читает, а машина вычисляет.

Предел никуда не делся, он переехал. Раньше рост системы упирался в то, сколько успевают прочитать люди. Теперь в то, сколько успевает проверить машина. Это разные пределы. Второй двигается вместе с железом, первый вместе с числом нанятых людей. На порядки дальше.

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

А то, что нельзя описать не тьюринг полным языком, надо ревьюить человеком и постоянно донастраивать харнес, если использовать ИИ-агентов. Или кодить без ИИ и ревьюить смыслы вручную.

Но даже если ИИ пишет на декларативном языке и проверка становится вычислением, то узкое место теперь не написание и не проверка. Узкое место это формулировка того, что должно быть истинно. Люди остаются единственными, кто может сказать, что мы хотим получить и зачем.