Bend : un langage avec preuves formelles pour bloquer les erreurs d'IA, exécutable sur GPU
En bref
- Bend est un langage conçu pour des AI agents qui compile en code natif rapide et supporte le parallélisme GPU. Il introduit LAWS.bend, un mécanisme de preuves formelles permettant de bloquer les modifications de code qui violent des invariants déclarés.
- Le projet affiche 20K étoiles sur GitHub mais suscite des doutes : historique Git supprimé, peu de forks/issues comparé à d'autres langages, et la complexité pratique des preuves reste opaque.
Ce que dit la source
L'auteur pose ce diagnostic : les humains vont cesser d'écrire du code post-AGI, mais il faut un moyen non-ambigu de spécifier les intentions aux systèmes d'IA. Bend y répond en combinant trois éléments : une exécution rapide (C-like sur CPU, parallélisation GPU), un vérificateur de type fondé sur des preuves (inspiré de Lean/Rocq) extrêmement rapide (< 1 seconde), et LAWS.bend, où les développeurs énoncent des lois que le code ne peut jamais transgresser sous peine de blocage à la compilation.
- Parallélisme automatique sans threads ni locks : découper une tâche en deux, Bend la propage sur tous les cœurs disponibles, puis les résultats sont fusionnés ; le langage affiche un exemple avec 4 096 cœurs GPU.
- Compilation ultra-rapide : le vérificateur de type (qui est aussi un vérificateur de preuve) prend moins d'une seconde, contre plusieurs minutes pour Lean ou Rocq sur du code de taille moyenne.
- LAWS.bend bloque les modifications qui violent une loi déclarée : l'exemple du jeu montre comment l'IA est forcée de réessayer jusqu'à générer une preuve que la loi tient.
- Le langage est jeune : aucun historique Git public, peu de forks (500) et de tickets (< 300 fermés/ouverts) comparé à d'autres langages de même taille d'audience (Gleam 1K forks, Zig 3K).
- La documentation technique de LAWS.bend est succincte ; plusieurs commentaires soulignent que passer des lois en pratique (écrire une preuve qu'un tri est correct, par exemple) demande une charge de travail importante et peu documentée.
Dans les commentaires
Débat partagé et polarisé : enthousiasme pour l'idée fondamentale (preuves formelles légères pour AI agents), mais scepticisme massif sur la maturité, la transparence du projet et l'applicabilité pratique. Peu de discussion substantielle sur les performances ou les cas d'usage réels.
- Plusieurs commentateurs questionnent si l'effort de rédaction et de preuve des lois est vraiment plus simple que celui de coder directement. Un commentateur relève que même demander à Claude de prouver une invariante triviale génère 100 K+ tokens en boucle d'essais-erreurs, ce qui suggère un coût cognitif élevé en pratique.
- L'absence d'historique Git, de releases versionnées et le faible nombre de forks/PRs par rapport à 20K étoiles soulèvent des doutes : ce pattern est atypique pour un vrai projet. L'auteur réplique qu'il a travaillé seul 16h/jour pendant un an ; un commentateur note que c'est précisément ce qui rend difficile la légitimité perçue.
- Un testeur rapporte que l'IA agent se perd dans des boucles de génération de patches pour satisfaire les lois, au lieu de reconnaître que la demande est incompatible avec la loi existante. Résultat : gâchis de tokens, patches bancals (par ex. rendre le plateau symétrique pour empêcher la triche, au lieu de refuser l'ajout).
- Confusion sur le périmètre de la preuve : un commentateur demande explicitement comment Bend prouve des invariantes sur des espaces d'états très grands (ex: jeu multidimensionnel), sans réponse technique détaillée visible dans les commentaires fournis. L'analogie avec Lean ne suffit pas à clarifier le mécanisme.
- Un accointance ancienne du projet (depuis mid-2023) relève que HN attendait plutôt une discussion sur les cas d'usage et les limitations, mais a reçu à la place une polarisation cosmétique entre défense du projet et critique des red flags administratifs.
Alternatives citées : Code Contracts (code-contracts.cc) est mentionné comme alternative co-localisant code et preuves.
Notre lecture
Bend porte une idée sérieuse : formaliser les invariantes d'une codebase et les vérifier syntaxiquement évite certaines classes d'erreurs. Pour un AI agent qui génère du code, c'est un levier théorique solide. Mais entre la théorie et une utilisation quotidienne, plusieurs fossés : 1) l'effort réel de rédaction des lois n'est pas documenté et ressort pénible en pratique ; 2) le projet souffre d'une transparence insuffisante (historique Git, versioning, changelogs) qui crée du doute sur sa viabilité long terme, au-delà des mérites techniques ; 3) l'efficacité sur des problèmes complexes (mondes d'état énormes) reste non démontrée. Pour une DSI : à surveiller en tant que recherche intéressante, mais pas d'adoption imminente. L'auteur a de bonnes intentions et un concept porteur, mais le projet a besoin d'une vraie infra open source avant de devenir fiable. Le buzz initial masque une exécution immature.