Bend 2, un langage rapide qui empêche les erreurs de l'IA grâce à des preuves, ce qui permet de vérifier que l'IA a correctement mis en œuvre les instructions génératives
Bend 2, un langage rapide qui empêche les erreurs de l'IA grâce à des preuves, ce qui permet de vérifier que l'IA a correctement mis en œuvre les instructions, et grâce auquel les intentions peuvent être formulées avec plus de précision. Grâce aux lois, les intentions peuvent être bien plus précises qu’en langage naturel. Grâce aux preuves, on peut vérifier que l’IA a correctement mis en œuvre nos instructions. Et un compilateur rapide l’exécute à grande vitesse.
Dans l’économie post-AGI, les humains finiront par ne plus écrire ni lire de code, mais nous aurons toujours besoin d’un moyen sans ambiguïté pour indiquer aux IA qui construisent le monde qui nous entoure ce que nous voulons qu’elles fassent. Grâce aux lois, nos intentions peuvent être bien plus précises qu’en langage naturel. Grâce aux preuves, nous pouvons vérifier que l’IA a correctement mis en œuvre nos instructions. Et un compilateur rapide l’exécute à grande vitesse. C’est ça, Bend : un langage rapide qui empêche les erreurs de l’IA grâce à des preuves, compilant la vitesse du C, le parallélisme CUDA, des preuves allégées, et la syntaxe Python.
Bend s’exécute rapidement : Bend se compile en code natif. Sur un seul cœur, il s’exécute presque aussi vite que le C. Le même binaire s’exécute également sur seize cœurs, ou sur le GPU, avec une vitesse pouvant atteindre cent fois celle d’un seul cœur.
Bend se compile rapidement : Le vérificateur de types de Bend est un vérificateur de preuves, comme dans Lean et Rocq. Ces opérations peuvent prendre plusieurs minutes sur une base de code de taille moyenne. Bend ne prend qu’une seconde au maximum, ce qui permet à un agent IA de vérifier après chaque modification.
Bend est parallèle : Pas de threads, pas de verrous, pas de noyaux à écrire. Divisez le travail en deux, et Bend répartit les appels sur tous les cœurs qu’il peut trouver, puis les regroupe.
Bend bloque les erreurs – grâce à la preuve : Comment faire confiance à un code que vous n’avez jamais lu ? En exigeant une preuve. C’est dans LAWS.bend que vous déclarez les lois. À partir de là, aucune IA ne peut jamais livrer une seule ligne qui les enfreigne.
Sans LAWS.bend, le bug a été mis en production. Avec LAWS.bend, l’IA a dû réessayer jusqu’à ce qu’elle construise un mur et prouve que la règle est respectée. Intégrer un bug est mathématiquement impossible : c’est un théorème.
LAWS.bend
1
2
3
4
5
| # LAW: no move sequence leads to victory.
law you_cant_win:
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False{} # never leads to victory |
PROOF.bend
1
2
3
| # PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
# ... written by the AI |
LAWS.bend est une version de AGENTS.md étayée par des preuves. « Ne commettez aucune erreur » fait désormais l'objet d'une vérification de types.
Pour commencer
Installation
curl -fsSL https://bend-lang.com/install.sh | sh
Demandez à votre agent d’utiliser Bend
Ajoutez ceci à votre fichier AGENTS.md :
1
2
3
4
5
| 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 |
Ensuite, dites simplement : « utilise Bend » !
Profitez d’applications sans bug, rapides et codées avec fluidité !
Astuces : demandez-lui d’écrire des lois pour tout ce qui ne doit jamais planter, et de paralléliser tout ce que vous souhaitez voir s’exécuter rapidement. Bend est encore jeune : si quelque chose ne fonctionne pas, demandez-lui d’ouvrir un ticket. Bend fonctionne mieux en back-end, sous Linux et macOS.
Sources : Présentation de Bend, Dépôt GitHub
Et vous ?
Pensez-vous que ce langage est crédible ou pertinent ?
Quel est votre avis sur le sujet ?
Voir aussi :
Quel est le meilleur langage pour les agents IA ? Un développeur Go avec 8 ans d'expérience affirme que Go surclasse ses concurrents, en se basant sur son expérience avec Bruin, son outil ETL CLI open source
Python reste numéro 1, R gagne en popularité et atteint son meilleur classement historique avec la 8e place, Java a pris de l'élan avec Java 26, tandis que MATLAB et SAS sont les grands perdants, selon TIOBE
L'IA abaisse les barrières mais amplifie les mauvais patterns : les données Octoverse de GitHub révèlent la mécanique silencieuse qui redistribue les parts de marché entre langages de programmation
Bend : un langage rapide qui empêche les erreurs de l’IA grâce à des preuves
Répondre avec citation
Partager