Об этом проекте

Bend 2 — новый язык программирования, разработанный для эпохи пост-AGI, где люди передают намерения ИИ-системам через язык без неоднозначностей. Его ключевая инновация — LAWS.bend: механизм, где разработчики объявляют инварианты (законы), которые ИИ должен математически доказать для любых изменений кода, что делает математически невозможным слияние ошибок, нарушающих эти правила. Основные возможности, указанные в README: **Производительность**: Нацелен на скорость уровня C на CPU и уровня CUDA на GPU. Бенчмарки показывают конкурентоспособную однопоточную производительность и масштабный параллелизм на тысячах ядер. Компилятор использует строгие типы, чистоту и линейность для оптимизации. **Проверка доказательств**: Заявляется проверка на порядки быстрее, чем в Isabelle, Agda, Lean или Coq, с проверкой сложных доказательств менее чем за секунду. **Неявный параллелизм**: Не нужно писать потоки, блокировки или ядра. Функции «разделяй и властвуй» автоматически распределяются по всем доступным ядрам CPU/GPU. Пример показывает pow2(20), распределённый по 4096 ядрам GPU. **Рабочий процесс с ИИ**: Разработан для разработки с помощью ИИ. Разработчики пишут законы в LAWS.bend (например, «сумма балансов должна быть нулевой», «игроки не могут проходить сквозь стены»), затем требуют от ИИ запустить `bend PROOF.bend` перед коммитом. Компилятор механически обеспечивает выполнение доказательств. **Особенности языка**: Синтаксис в стиле Python с зависимыми типами. Аффинная/линейная система типов (значения нельзя разделять). Требуется завершающаяся рекурсия (с escape-механизмом @unsafe). Целевые платформы: C, Metal, CUDA, JavaScript. Базовая библиотека минимальна; эффекты включают I/O, каналы, TCP/UDP, доступ к файлам. **Текущие ограничения (явно перечисленные)**: Многословные аннотации, нет классов типов/трейтов/макросов, нет тактик или поиска доказательств, ограниченные числовые типы (только Nat, U32, F32), медленные строки (связные списки), нет HTTP/JSON/TLS/regex, одна GPU на программу, нет инкрементальной компиляции, медленная нативная компиляция, минимальный инструментарий (нет LSP, отладчика, форматтера, REPL), компилятор в основном написан ИИ и не проверен. Проект включает формализацию в Lean (bend.lean), академические статьи (теория типов BendTT, рантайм BendRT) и растущую коллекцию демо. Каналы сообщества: Discord, Reddit, X/Twitter. Лицензия не указана в предоставленном материале.