bend

Bend 2 est un nouveau langage de programmation conçu pour l'ère post-AGI, où les humains communiquent leur intention aux systèmes d'IA via un langage sans ambiguïté. Son innovation centrale est LAWS.bend — un mécanisme où les développeurs déclarent des invariants (lois) que l'IA doit prouver mathématiquement pour toute modification de code, rendant mathématiquement impossible de fusionner des bogues violant ces règles. Capacités clés démontrées dans le README : **Performance** : Vise la vitesse de niveau C sur CPU et de niveau CUDA sur GPU. Les benchmarks montrent des performances monocœur compétitives et une mise à l'échelle parallèle massive sur des milliers de cœurs. Le compilateur exploite les types forts, la pureté et la linéarité pour l'optimisation. **Vérification de preuves** : Revendique une vérification des ordres de grandeur plus rapide qu'Isabelle, Agda, Lean ou Coq, vérifiant des preuves complexes en moins d'une seconde. **Parallélisme implicite** : Pas de threads, verrous ou kernels à écrire. Les fonctions diviser-pour-régner se répartissent automatiquement sur tous les cœurs CPU/GPU disponibles. L'exemple montre pow2(20) distribué sur 4 096 cœurs GPU. **Flux de travail collaboratif avec l'IA** : Conçu pour le développement assisté par IA. Les développeurs écrivent des lois dans LAWS.bend (par exemple, « la somme des soldes doit être zéro », « les joueurs ne peuvent pas traverser les murs »), puis exigent que l'IA exécute `bend PROOF.bend` avant de committer. Le compilateur applique mécaniquement les preuves. **Caractéristiques du langage** : Syntaxe de type Python avec types dépendants. Système de types affines/linéaires (les valeurs ne peuvent pas être partagées). Récursion terminante requise (avec échappatoire @unsafe). Cibles : C, Metal, CUDA, JavaScript. La bibliothèque de base est minimale ; les effets incluent I/O, canaux, TCP/UDP, accès fichiers. **Limitations actuelles (listées explicitement)** : Annotations verbeuses, pas de classes de types/traits/macros, pas de tactiques ou recherche de preuves, types numériques limités (Nat, U32, F32 uniquement), chaînes lentes (listes chaînées), pas de HTTP/JSON/TLS/regex, un seul GPU par programme, pas de compilation incrémentale, compilation native lente, outillage minimal (pas de LSP, débogueur, formateur, REPL), compilateur largement écrit par IA et non audité. Le projet inclut une formalisation en Lean (bend.lean), des articles académiques (théorie des types BendTT, runtime BendRT) et une collection croissante de démos. Canaux communautaires : Discord, Reddit, X/Twitter. Licence non spécifiée dans le matériel fourni.