Bend : un langage à vérification de preuve qui bloque les erreurs de l'IA sur CPU et GPU

Bend est un langage compilé et parallèle conçu pour le code généré par IA. Sa promesse centrale : plutôt que de faire confiance à un résultat que vous ne lisez jamais, vous déclarez des lois dans un fichier LAWS.bend et exigez que l'agent les prouve avant toute fusion.

Le discours ressemble à celui de tous les autres outils de codage IA, mais la mécanique diffère. Le vérificateur de types de Bend est un vérificateur de preuves, le même principe que Lean ou Rocq. La différence mise en avant, c'est la vitesse : ces vérificateurs peuvent prendre des minutes sur des bases de code de taille moyenne, tandis que Bend revendique une seconde au maximum, permettant à un agent de lancer les vérifications après chaque modification.

D'où vient cette rapidité

• Compile en code natif. Presque la vitesse du C sur un seul cœur.
• Le même binaire monte en puissance sur seize cœurs ou sur GPU. La documentation annonce jusqu'à 100 fois plus rapide qu'un seul cœur.
• Le parallélisme est automatique. Vous divisez le travail en deux ; Bend répartit les appels sur les cœurs ou les cœurs GPU, puis les joint. Ni threads, ni verrous, ni code noyau.

Le site montre un exemple pow2.bend tournant sur 4 096 cœurs GPU.

Les lois et le modèle de preuve

Vous écrivez une loi dans LAWS.bend :

# LAW: no move sequence leads to victory.
law you_cant_win : for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False

L'agent écrit ensuite la preuve correspondante dans PROOF.bend :

# PROOF: you_cant_win holds.
def Laws.you_cant_win (moves):
    # ... écrit par l'IA

Une fois une loi déclarée, le site affirme que l'agent ne peut pas fusionner une ligne qui la viole. La démo utilise un jeu : demandez à Claude de faire en sorte que le plateau se replie sur lui-même. Sans LAWS.bend, le bug est fusionné et livré. Avec, l'agent doit réessayer jusqu'à construire une preuve. La formulation dans la source : fusionner un bug devient « mathématiquement impossible ».

Installation

Installez :

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

Ajoutez ensuite ce bloc à votre AGENTS.md pour que les agents sachent quoi faire :

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

Bend traite essentiellement LAWS.bend comme un AGENTS.md soutenu par des preuves. « Ne faites pas d'erreur » devient vérifié par types.

Mises en garde de la source

La documentation est franche : Bend est jeune, attendez-vous à des bugs et signalez-les. Il fonctionne mieux côté back-end et cible Linux et macOS. Le cœur s'appuie sur deux articles — BendTT (théorie des types dépendants affines) et BendRT (runtime parallèle CPU/GPU).

À qui cela s'adresse

Aux équipes qui laissent des agents livrer du code qu'elles ne lisent pas, en particulier les services back-end où une règle comme « les soldes ne deviennent jamais négatifs » doit être appliquée plutôt que relue manuellement.