Bend: мова, що блокує помилки ШІ доведеннями

Bend подають одним рядком: швидка мова, яка блокує помилки ШІ доведеннями, поєднуючи швидкість C, паралелізм CUDA, доведення Lean і синтаксис Python. Аргумент проєкту такий: у пост-AGI економіці люди зрештою перестануть писати й читати код, але їм усе одно потрібен недвозначний спосіб сказати машинам, що будувати. Закони, стверджує сайт, виражають намір точніше за природну мову, доведення перевіряють, що модель реалізувала його правильно, а швидкий компілятор виконує результат.

Швидко виконується, швидко перевіряється

Bend компілюється в нативний код. На одному ядрі, за заявою сайта, продуктивність близька до C, а той самий бінарник розподіляється на шістнадцять ядер або на GPU, працюючи до ста разів швидше за одне ядро. Швидкість важлива й для перевірки: типізатор Bend — це перевіряч доведень у традиції Lean і Rocq, де перевірка середнього проєкту може тривати хвилинами. Bend витрачає щонайбільше секунду, і саме тому агент може перевіряти роботу після кожної зміни.

Паралелізм без потоків і ядер

Тут немає потоків, блокувань і ядер, які треба писати вручну. Програміст ділить роботу навпіл, а мова розкидає виклики по всіх доступних ядрах і збирає результати назад. У демо показано обчислення степеня двійки на 4096 ядрах GPU.

Закони як AGENTS.md, підкріплений доведенням

На питання, як довіряти коду, який ніхто не читав, Bend відповідає вимогою доведення. Закони оголошуються у файлі LAWS.bend, і після цього, за словами сайта, жоден агент не проведе рядка, що їх порушує. У прикладі правило гри стверджує, що жодна послідовність ходів не веде до перемоги: закон пишеться для довільного списку ходів, дошку повторюють від початку й доводять, що виграш не настає ніколи. Парний файл PROOF.bend, який пише ШІ, доводить, що закон виконується. В ілюстрації функція завертання дошки випустила реальний баг; після оголошення закону агент мусив повторювати спроби, доки не довів обмеження. Випустити баг стає, за формулюванням сайта, математично неможливо — це теорема.

Як почати

Встановлення — одна команда в shell, після чого інструкції звернені до кодових агентів: додайте в AGENTS.md короткий блок, який радить запускати bend guide, тримати важливі правила в LAWS.bend, перевіряти bend PROOF.bend перед кожним комітом і паралелити код усюди, де можливо. Сайт радить просити закони для всього, що не повинно ламатися ніколи, і починати з бекенду на Linux або macOS. Bend молодий, попереджають автори, тож багів варто очікувати й повідомляти про них; деталі — в посібнику мови на GitHub і в двох статтях, присвячених афінній залежній теорії типів, що становить ядро Bend, та паралельному середовищу для CPU і GPU.