Bend – A language that blocks AI mistakes via proof, on CPU and GPU
Bend — это быстрый язык программирования с синтаксисом, похожим на Python, который компилируется в нативный код и достигает скорости C на одном ядре, а на 16 ядрах или GPU — до 100x ускорения. Его ключевая особенность — встроенная система доказательств, вдохновлённая Lean и Rocq, которая позволяет формально проверять свойства кода. Типовый проверятель Bend работает за секунду, что делает его пригодным для использования ИИ-агентами после каждого изменения.
Благодаря LAWS.bend разработчики могут объявлять неизменяемые правила (например, «победа невозможно»), которые ИИ не может нарушить — любая попытка нарушить закон блокируется на этапе проверки. Пример с игрой показывает, что без LAWS.bend ИИ допускает ошибку (слияние клеток), а с ней — вынужден исправлять код, пока не докажет корректность. Bend автоматически параллелизует код без потоков или блокировок, распределяя вычисления по доступным ядрам или GPU-ядрам. Для начала работы достаточно установить Bend через скрипт и добавить рекомендации в AGENTS.md: запускать bend guide, соблюдать LAWS.bend, проверять PROOF.bend перед коммитом и параллелизовать всё возможное. Язык ориентирован на бэкенд, Linux и macOS, и позиционируется как инструмент для создания надёжных, высокопроизводительных систем в эпоху ИИ-генерируемого кода.