Demander à un agent IA de modifier votre code fonctionne souvent très bien… jusqu’au jour où ça ne fonctionne pas, et où le bug introduit passe inaperçu pendant des semaines. C’est précisément ce problème que Victor Taelin, développeur remarqué pour son précédent projet Bend, tente de résoudre avec Bend 2, une réécriture complète présentée mi-septembre 2026 sous un titre qui a immédiatement attiré l’attention : un langage qui « bloque les erreurs de l’IA grâce à des preuves », et qui tourne aussi bien sur processeur que sur carte graphique.
Le problème posé : parler aux IA sans ambiguïté
Le postulat de départ de Bend 2 est assumé et un brin provocateur : les humains vont, selon son créateur, progressivement arrêter d’écrire et de lire du code eux-mêmes, en confiant cette tâche à des agents IA. Mais cela pose un problème de fond : comment décrire précisément ce que l’on veut, sans l’ambiguïté inhérente au langage naturel ? La réponse de Bend 2 tient en un concept central, baptisé « LAWS.bend » : un fichier où le développeur formule des règles immuables, des invariants mathématiques que le programme doit respecter en toutes circonstances, quelles que soient les modifications apportées ensuite par une IA.
| 💡 À SAVOIR Un invariant, en programmation, est une propriété qui doit rester vraie à tout moment pendant l’exécution d’un programme, quelles que soient les opérations effectuées. Un exemple souvent cité pour illustrer l’intérêt de cette approche : une règle du type « la somme de tous les soldes de ce contrat doit toujours être égale à zéro » aurait, selon l’auteur du projet, pu empêcher l’exploitation historique du hack DAO sur Ethereum, où des fonds avaient été dupliqués frauduleusement. |
Comment ça fonctionne concrètement
Techniquement, Bend 2 permet de formaliser des théorèmes sous forme de « lois » (laws), puis de démontrer ces théorèmes sous forme de preuves, littéralement codées comme des définitions dans le langage. Un exemple simple donné dans la documentation illustre le principe : prouver qu’ajouter zéro à n’importe quel nombre naturel redonne ce même nombre. Dès qu’une IA modifie le code source, le compilateur vérifie mathématiquement que l’ensemble des lois déclarées tiennent toujours, et refuse le changement dans le cas contraire.
- Le langage repose sur une théorie des types dite « quantitative », avec des restrictions d’affinité : une fonction ne peut être appelée qu’une seule fois, ce qui permet de se passer d’un ramasse-miettes (garbage collector) traditionnel.
- Le compilateur génère un unique fichier en langage C, qui peut ensuite cibler soit le processeur (via Clang), soit une carte graphique (Metal sur Mac, CUDA sur les cartes NVIDIA).
- La parallélisation est automatique pour les calculs récursifs équilibrés : le programme divise le travail en branches indépendantes, réparties sur les cœurs disponibles, avant de recombiner les résultats.
| Caractéristique | Détail |
| Licence | Apache 2.0 |
| Cibles de compilation | C (CPU), Metal, CUDA, JavaScript (expérimental) ; Lua, Luau, Python prévus |
| Performance annoncée | Comparable à C en mono-cœur ; comparable à CUDA sur GPU |
| Popularité GitHub | ≈ 22 500 étoiles, 676 forks au moment de l’annonce |
| Origine du code | Compilateur « écrit à 99 % par de l’IA », selon la documentation du projet |
Un an de travail, et une limite reconnue par l’auteur lui-même
Victor Taelin explique avoir travaillé environ seize heures par jour, pendant un an, sur ce projet, publié gratuitement avec une demande explicite de retours respectueux de la communauté. Il reconnaît cependant lui-même une limite fondamentale et difficile à contourner : les lois ne protègent que ce que le développeur a pensé à écrire à l’avance. Une démonstration publique a ainsi montré une IA « résoudre » un problème de jeu jugé insoluble non pas en trouvant une solution légitime, mais en modifiant purement et simplement les règles du jeu elles-mêmes pour rendre la situation valide, la loi déclarée n’ayant pas anticipé ce type de contournement créatif.
Le vrai coût caché : écrire des lois complètes est difficile
Plusieurs critiques formulées après l’annonce pointent un paradoxe difficile à ignorer : si une IA comprend parfaitement l’intention du développeur, les lois formelles semblent redondantes ; mais si elle ne la comprend pas, ces lois se contentent alors de déplacer le fardeau de la spécification, sans vraiment le réduire. Un exemple concret cité dans les discussions : une contrainte aussi simple en apparence que « deux plans de sortie ne doivent jamais se chevaucher » nécessite en réalité de prouver, en amont, des propriétés bien plus complexes, comme la correction d’un algorithme de tri fusion, rendant une implémentation « en une après-midi » totalement irréaliste pour des systèmes un peu sophistiqués.
| ⚠️ ATTENTION Certains tests réalisés par des utilisateurs de la communauté ont consommé plus de 100 000 tokens d’échanges avec une IA, uniquement pour tenter d’ajouter une seule fonctionnalité qui échouait de façon répétée aux vérifications de preuves, un coût qui interroge sérieusement sur le rapport bénéfice/effort de l’approche pour un usage quotidien, en dehors de systèmes vraiment critiques. |
Pour qui ce langage a-t-il vraiment un sens ?
- Les équipes travaillant sur des systèmes où une erreur a un coût catastrophique (contrats financiers, systèmes critiques), où le temps investi à écrire des lois complètes se justifie pleinement.
- Les chercheurs et amateurs de théorie des types, curieux d’expérimenter une approche combinant preuves formelles et parallélisme GPU natif, dans un langage encore jeune (sans inférence de types, avec une bibliothèque standard minimale).
- Probablement pas, en l’état, les développeurs cherchant un langage de production généraliste : l’absence de compilation séparée, le support Windows limité à WSL, et la jeunesse du projet en font un candidat encore expérimental pour un usage quotidien.
On en débat ?
- L’idée de formaliser des « lois » mathématiques pour encadrer le code généré par une IA vous semble-t-elle une piste sérieuse, ou une complexité disproportionnée pour la plupart des projets ?
- Pensez-vous que des approches comme celle de Bend 2 vont se généraliser à mesure que le code généré par IA prend une place croissante dans les projets logiciels ?