Bend: язык, который блокирует ошибки ИИ с помощью математических доказательств

Проект Bend предлагает необычный ответ на вопрос, который всё чаще возникает в эпоху "вайб-кодинга": как доверять коду, который вы никогда не читали? Ответ авторов прост — потребовать доказательство.

Идея

Авторы исходят из смелого допущения: в "пост-AGI экономике" люди перестанут писать и читать код, но им по-прежнему нужен способ однозначно объяснить ИИ, что именно требуется. Естественный язык для этого слишком расплывчат, поэтому Bend предлагает описывать намерения в виде законов, а корректность реализации подтверждать доказательствами. Синтаксис при этом близок к Python.

Как это работает

Центральный элемент — файл LAWS.bend, куда разработчик записывает правила, которые никогда не должны нарушаться. С этого момента, по замыслу авторов, ни один ИИ не сможет отправить строку кода, ломающую закон. Проверка типов в Bend одновременно является проверкой доказательств — как в Lean или Rocq. Разница, по утверждению создателей, в скорости: если полноценные пруф-чекеры тратят на средний проект минуты, то Bend укладывается в секунду, что позволяет агенту проверять код после каждого изменения.

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

Скорость и параллелизм

Bend компилируется в нативный код и на одном ядре работает почти как C. Тот же бинарник запускается на шестнадцати ядрах или на GPU, ускоряясь, по заявлениям, до ста раз относительно одного ядра. Параллелизм подаётся как бесплатный бонус: ни потоков, ни блокировок, ни ядерных функций писать не нужно — задача разбивается надвое, распределяется по всем доступным ядрам и собирается обратно. В демонстрации функция pow2 работает на 4096 ядрах GPU.

Как попробовать

Установка сводится к запуску скрипта через curl, после чего в AGENTS.md добавляется инструкция для агента: изучить язык командой bend guide, хранить правила в LAWS.bend и запускать bend PROOF.bend перед коммитом. По сути, LAWS.bend — это "AGENTS.md, подкреплённый доказательством": фраза "не делай ошибок" наконец становится проверяемой типами.

Сами авторы честно предупреждают, что проект молодой: лучше всего он работает на бэкенде под Linux и macOS, а баги стоит ожидать и сообщать о них. В основе языка лежат две работы — BendTT (аффинная зависимая теория типов) и BendRT (параллельный рантайм для CPU и GPU).

Источник: Hacker News