Bend 2: язык, где AI-коммиты требуют машинно-проверяемых доказательств

Bend

инструменты офиц. + СМИ 3 ист. ~1 мин

Bend 2 (репозиторий bendlang/bend, активен 18 сентября) — язык, где инварианты живут в файле LAWS.bend, и любое изменение, автором которого является AI, должно поставляться с PROOF.bend, машинно проверяемым против них: тайпчекер doubling as proof-checker (в стиле Lean/Rocq) отклоняет нарушающие правки до коммита, при этом заявлены single-binary масштабирование на CPU/GPU и однокоростная скорость уровня C.

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

Формализует идею «спеки, из которой AI не выкрутится», в механизм enforcement: класс багов, доехавших до merge, становится доказуемо пустым для проверяемых свойств.

Важность: 2/5

Заметный релиз нового языка программирования, высокое внимание сообщества

programming-languages formal-reasoning compiler open-source

Источники

официальный Bend — a language that blocks AI mistakes via proof

официальный bendlang/bend — Bend 2 (20.6k stars)

СМИ HN: Bend (355 points, Sep 17)