Bend и борьба с тихими багами

Знаете, что самое страшное в мире AI-кодинга? Тихие баги. AI сгенерирует код, всё выглядит прилично, тесты проходят — а потом в продакшене что-то ломается. И ты даже не знаешь, где именно. Традиционное тестирование не спасает: нельзя написать тест на каждую возможную последовательность действий.

Мне попался интересный проект — Bend. Это язык программирования, который пытается решить фундаментальную проблему: как заставить AI писать код без скрытых ошибок?

В чём суть

Bend — это язык с проверкой через формальные доказательства. Суть простая: вы описываете законы — что должно быть всегда верно в вашем коде. Например, «в этой игре невозможно выиграть» или «баланс счёта никогда не станет отрицательным». Потом AI пишет код и формальное доказательство того, что код не нарушает эти законы. Если proof не сходится — компиляция не пройдёт.

Тест проверяет конкретный случай, а формальное доказательство может охватывать все случаи в рамках заданного утверждения. Это не гарантия отсутствия любых багов: неверно сформулированный закон, неполная спецификация или ошибка инструментов остаются рисками.

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

Файл LAWS.bend — это место, где вы объявляете законы:

## Закон: ни одна последовательность ходов не ведёт к победе

law you_cant_win: for moves: List<Move>
board = replay(start(), moves)
is_won(board) == False

Файл PROOF.bend — AI пишет доказательство того, что закон выполняется.

Авторы провели эксперимент: попросили AI добавить фичу в игру — «доска зацикливается». Без формальных законов баг прошёл в продакшен. С Bend — AI пришлось переписывать код, пока proof не подтвердил, что закон всё ещё соблюдается. Слияние бага стало математически невозможным.

BEND: АРХИТЕКТУРА КОМПИЛЯЦИИ И ВЫПОЛНЕНИЯ
─────────────────────────────────────────
┌─────────────┐    ┌──────────────┐    ┌──────────────┐
│  .bend      │───▶│  Компилятор  │───▶│  CUDA/GPU    │
│  LAWS.bend  │    │  (proof      │    │  или          │
│  PROOF.bend │    │   checker)   │    │  Native CPU  │
└─────────────┘    └──────────────┘    └──────────────┘
       │                 │                    │
       ▼                 ▼                    ▼
  Законы и       Проверка: proof    Распараллеливание
  ограничения    vs. законы        на ядра/GPU

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

По данным авторов, Bend компилируется в нативный код и в их тестах приближается к C на одном ядре. Вычисления можно распараллеливать на CPU или GPU; заявленное ускорение до 100 раз относится к параллельным примерам относительно одного ядра, а не к любой программе на 16-ядерном CPU.

ПРОВЕРКА И СКОРОСТЬ
───────────────────
┌──────────────┐     ┌──────────────┐
│ Изменение    │────▶│ Проверка     │
│ кода         │     │ proof        │
└──────────────┘     └──────────────┘
       │                    │
       ▼                    ▼
┌──────────────┐     ┌──────────────┐
│ CPU          │────▶│ GPU / ядра   │
│ Native code  │     │ параллельно  │
└──────────────┘     └──────────────┘

Авторы заявляют быструю проверку доказательств в своих примерах, чтобы агент мог запускать её после каждого изменения. Это результат их демонстрации, а не универсальная оценка времени для всех проектов или сравнение с любой задачей в Lean.

Синтаксис и установка

Синтаксис — почти Python. Это сознательное решение: чтобы AI-агенты могли легко писать код, а люди — его читать.

Установка тривиальна:

curl -fsSL https://bend-lang.com/install.sh | sh

Для AI-агентов рекомендуют добавить в AGENTS.md:

• Запускать bend guide для обучения
• Использовать LAWS.bend для важных правил
• Проверять bend PROOF.bend перед коммитом
• Параллелить код где возможно

Практический вывод

Bend — это интересный эксперимент на стыке языков программирования, формальной верификации и AI. Идея «законы + доказательства = защита от багов» элегантна. Особенно для AI-генерируемого кода, где тихие ошибки — норма.

Но есть нюансы. Язык молодой, экосистема только формируется, и пока неясно, как это масштабируется на большие проекты. Proof-системы традиционно требуют глубокой экспертизы — здесь авторы упростили, но насколько это работает на практике, покажет время.

Тем не менее, направление правильное. Даже если Bend не станет мейнстримом, сама идея — писать законы, а не тесты — заслуживает внимания.

Кстати, если хотите покопаться в коде — Bend на GitHub.

Выводы

• Bend предлагает защищать код не тестами, а формальными законами и доказательствами.
• Это особенно полезно для AI-генерируемого кода, где скрытые ошибки трудно поймать.
• Быстрая проверка proof и параллельное выполнение делают идею практичнее классических proof-систем.
• Проект ещё молод, но направление выглядит перспективным.

Ссылки

• Bend — язык для защиты AI-кода через proof и параллельное выполнение
• Bend на GitHub — исходный код проекта и документация