Автор рассматривает современное увлечение AI через программу математика Давида Гильберта и его лозунг «Мы должны знать — мы будем знать». Парадоксы наивной теории множеств, включая парадокс Рассела о множестве всех множеств, не содержащих себя, вызвали кризис оснований математики. Гильберт стремился создать полную и непротиворечивую систему аксиом, из которой можно было бы выводить математические истины без парадоксов.
Теоремы Гёделя о неполноте показали невозможность такой самодостаточной системы. Тьюринг закрыл связанную задачу об универсальном алгоритме проверки истинности любого утверждения, доказав неразрешимость проблемы остановки. При этом теория типов получила развитие и легла в основу интерактивных систем доказательства теорем вроде Lean, где программа проверяет формализованные рассуждения. По мысли автора, AI-агенты в сочетании с такими механизированными системами неожиданно приблизили «машину доказательств», о которой мечтал Гильберт.
В программировании автор видит опасную противоположную реакцию: отказ читать сгенерированный код становится обычной практикой. Он считает это трагедией для дисциплины, где по исходному коду в принципе можно детально понять поведение программы. Успешные тесты и даже формальная верификация, по его мнению, не должны заменять понимание.
Сравнение с математикой здесь буквальное благодаря соответствию Карри — Ховарда: программа может рассматриваться как доказательство, и именно на таких принципах работают proof assistants. Если созданное AI доказательство слишком длинно, математики упрощают его до доступной человеку формы. Автор предлагает программистам поступать так же — применять абстракции, рефакторинг, сужать область ответственности, создавать и внедрять высокоуровневые языки, пока код снова не поместится в голове.
Это эссе выражает позицию специалиста по computer science, а не сообщает результат эксперимента. Автор не утверждает, что знает пределы возможностей AI, но предупреждает: бездумное принятие ответов машины лишает человека контроля. В качестве практического ответа он призывает сохранять понимание вычислений и присоединяться к инициативе People of Programming, защищающей ценность программирования за пределами автоматической генерации.