18 septembre 2026 Bend sert d'exemple utile à mon point général concernant le vibe-coding, car il est récent, de haut profil et présente des aspects qui le rendent facile à utiliser comme exemple. Je ne sais rien de l'historique de l'auteur dans la conception de langages ou s'il a réellement considéré les compromis ci-dessous et pris ce que je pense être un mauvais choix. N'hésitez pas à remplacer « l'auteur » ci-dessous par « un auteur hypothétique qui aurait pu créer la même chose ».

Je n'aime évidemment pas les décisions de conception prises dans Bend et je voulais les présenter, cependant cela a été excessivement confondu avec le point principal que j'essaie de faire valoir ci-dessous. Je ne veux pas modifier cela maintenant et faire croire que les commentaires existants sont excessivement sévères, donc je pense que la meilleure solution est d'expliquer quel était mon modèle mental de l'article pendant que je l'écrivais. Voici un commentaire de l'auteur de Bend.

Bend 2 est présenté comme un langage pour l'ère du codage par IA : les humains écrivent des « lois », l'IA écrit les implémentations et les preuves, et le compilateur vérifie que les preuves sont solides. Tout cela semble assez impressionnant et je peux comprendre pourquoi quelqu'un voudrait un langage qui fait cela. Il y a en fait quelques problèmes majeurs avec cette idée ; cependant, ce n'est pas le sujet de cet article.

Au lieu de cela, je veux parler de la façon dont Bend lui-même semble être tombé dans un piège courant lié au vibe-coding que je ne vois pas mentionné souvent. Commençons par une base de ce que Bend exige du développeur pour écrire pour sa démonstration sur la page d'accueil :https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend Je ne le reproduirai pas ici car le code n'est pas trop important. Ce qui est important pour cet article est qu'il contient assez de code.

Il comporte 58 lignes de code juste pour indiquer que le joueur ne peut jamais toucher le drapeau ou gagner la partie. Il y a aussi d'autres problèmes dans le fait que le LLM peut redéfinir les sous-programmes Game pour faire n'importe quoi ; cependant, cela n'est pas non plus le point de l'article. Ensuite, voyons ce que le LLM qui écrit le code pour ce programme doit écrire afin de prouver les « lois » :https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend C'est beaucoup. 442 lignes de code pour prouver ces propriétés simples.

Alors, quel est mon problème avec ceci ? Pourquoi est-ce que je l'appelle un piège du vibe-coding ? Le problème est que le vibe-coding permet de construire une solution substantielle avant d'avoir suffisamment appris sur le problème pour reconnaître qu'une meilleure solution existe. Un développeur peut produire un langage et un compilateur entiers tout en manquant une approche qu'une enquête d'introduction au domaine aurait placée directement devant eux. Le domaine en question est la vérification formelle.

Il est remarquable que ces deux mots n'apparaissent nulle part sur la page web de Bend ou dans sa base de code. Le développeur a construit un langage entier autour d'un domaine apparemment sans réaliser que ledit domaine existe. Pour démontrer clairement pourquoi ceci est un problème, recréons le même programme que Bend utilise comme démonstration dans SPARK, un langage et un compilateur open source pour la vérification formelle.

Pour être juste envers Bend, j'ai moi-même fait du vibe-coding pour cela, j'ai simplement dit à un LLM de recréer la démonstration en SPARK sans aucun conseil supplémentaire :package Game with SPARK_Mode issubtype Column is Integer range 0 .. 11;subtype Row is Integer range 0 .. 7;type State is record X : Column; Y : Row; Won : Boolean;end record; Start : constant State := (8, 5, False);function Wall (X : Column; Y : Row) return Boolean is(((X = 3 or X = 11) and Y <= 3)or ((Y = 3 or Y = 7) and X <= 3));function Cell (X : Column; Y : Row) return Character is(if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');-- Inductive invariant: outside the sealed room, off walls, not won.function Safe (G : State) return Boolean is((G. X > 2 or G. Y > 2) and not Wall (G.

X, G. Y) and not G. Won)with Ghost;procedure Step (G : in out State; Key : Character)with Post => (if Safe (G'Old) then Safe (G));-- Both Bend laws, including the actual cell drawn by the terminal.function Replay (Keys : St...