ИИтог

Bend, язык программирования, который доказательствами блокирует ошибки ИИ-агентов

инструментыРедакция ИИтогHacker News🔥76Рейтинг ИИтог76Влияние60Новизна65Релевантность95Неожиданность55Участники25Достоверность82

На сайте bend-lang.com представлен Bend, язык программирования, который позиционируется как защита от ошибок, вносимых ИИ-агентами в код. Ключевая идея: в файле LAWS.bend разработчик формулирует правила («законы»), которые код обязан соблюдать всегда, а в PROOF.bend хранится доказательство того, что эти законы выполняются. Проверщик типов Bend устроен как доказатель теорем, по аналогии с языками Lean и Rocq (Coq). По утверждению авторов, там, где такие проверки в Lean и Rocq на кодовой базе среднего размера могут занимать минуты, у Bend это занимает не больше секунды, так что ИИ-агент способен прогонять проверку после каждого изменения.

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

Сценарий использования показан на примере игры: агенту (в демонстрации назван Claude) дают задачу «сделать так, чтобы поле заворачивалось по краям». Без файла LAWS.bend в код, по утверждению авторов, проходит баг; с LAWS.bend агент вынужден повторять попытки, пока не построит стену и не докажет, что закон (в примере, «эта последовательность ходов не ведёт к победе») выполняется. Авторы формулируют это как «слияние бага математически невозможно, это теорема».

Установка, через curl -fsSL https://bend-lang.com/install.sh | sh; предлагается добавить инструкции по работе с Bend прямо в AGENTS.md agent-инструмента, после чего достаточно сказать агенту «используй Bend». Проект описан как молодой: авторы прямо предупреждают, что стоит ожидать багов, и просят сообщать о них. На странице также упомянуты две технические статьи, про BendTT (аффинную зависимую теорию типов, ядро языка) и BendRT (параллельную среду выполнения для CPU и GPU). Bend, по словам авторов, лучше всего работает на бэкенде, под Linux и macOS. Источник, лендинг проекта; в тексте нет имени автора или компании, даты релиза, номера версии или методологии измерения производительности за заявлениями о скорости.

Ключевые факты

  • Bend, язык программирования, у которого проверщик типов работает как доказатель теорем (по аналогии с Lean и Rocq): в LAWS.bend задаются обязательные правила, в PROOF.bend, доказательство их соблюдения, и код, нарушающий правило, слить в проект нельзя.
  • По заявлению авторов, проверка занимает не больше секунды на кодовой базе среднего размера, против минут у Lean и Rocq, что позволяет ИИ-агенту гонять её после каждого изменения.
  • Один и тот же скомпилированный бинарник, по утверждению разработчиков, работает почти со скоростью C на одном ядре, параллелится на шестнадцать ядер CPU или на GPU (в демо, 4096 ядер), где ускорение доходит до ста раз без ручного написания потоков и ядер.
  • Установка, через install-скрипт, интеграция задумана через AGENTS.md agent-инструментов; проект называют молодым и прямо просят сообщать об ошибках.
  • На странице нет имени автора/компании, даты релиза, версии и методологии замеров производительности, все цифры о скорости взяты со слов самих разработчиков.

Почему это важно

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

Кому это важно

В первую очередь, разработчикам и командам, которые уже поручают написание кода ИИ-агентам (в примере на странице назван Claude) и хотят получить гарантию, что агент не сможет случайно или незаметно нарушить критичное для проекта правило, а также тем, кому нужна массовая параллельная обработка на CPU/GPU без ручного написания потоков.

Как это применить

Bend ставится однострочным скриптом (curl -fsSL https://bend-lang.com/install.sh | sh), после этого командой bend guide можно изучить язык. Практический паттерн: завести LAWS.bend с правилами, которые не должны нарушаться, PROOF.bend, с доказательством их выполнения, и прогонять bend PROOF.bend перед каждым коммитом. Разработчики предлагают прописать эти шаги прямо в AGENTS.md используемого агент-инструмента и затем просто говорить агенту «используй Bend».

Можно ли доверять

Источник, собственный лендинг проекта, то есть самоописание, а не независимый обзор. В тексте нет имени автора, компании, даты релиза или номера версии, а заявления о скорости («почти как C», «до ста раз быстрее на GPU») не сопровождаются описанием методологии, оборудования или конкретной задачи бенчмарка, их стоит воспринимать как маркетинговые цифры разработчиков, а не как проверенные независимо измерения.

Риски и подводные камни

Проект сам называет себя молодым и прямо предупреждает, что стоит ожидать багов. Гарантия «код, нарушающий закон, слить нельзя» работает ровно настолько хорошо, насколько правильно сформулирован сам закон в LAWS.bend, ошибка или неполнота в формулировке правила не будет поймана доказательством. Также заявлено, что Bend лучше всего работает на бэкенде и только под Linux и macOS, то есть область применения уже сейчас ограничена.

«Слияние бага математически невозможно: это теорема.»

— лендинг Bend (bend-lang.com)