Bend Language: Codice Corretto Dimostrato, Esecuzione Veloce su GPU

Bend: Un Nuovo Linguaggio che Rende gli Errori di Codifica dell'AI Matematicamente Impossibili

Nella corsa all'adozione dello sviluppo assistito dall'AI, è emerso un problema critico: come fidarsi del codice che non si è mai letto? Bend, un nuovo linguaggio di programmazione open-source di Higher Order Company, offre una risposta provocatoria: richiedere una dimostrazione matematica che il codice sia corretto prima di poterlo integrare.

Bend combina tre proprietà raramente coesistenti: velocità di esecuzione quasi pari al C, parallelismo automatico su core CPU e GPU, e un sistema di tipi dipendenti abbastanza potente da verificare il comportamento del programma. Il risultato è un linguaggio progettato per l'era post-AGI, in cui gli umani specificano l'intento attraverso 'leggi' precise e gli agenti AI generano codice che deve dimostrare la conformità.

Controllo delle Dimostrazioni come Barriera ai Bug

Al centro di Bend c'è un flusso di lavoro innovativo. Gli sviluppatori scrivono leggi in un file LAWS.bend, dichiarando invarianti che non devono mai essere infranti. Quando un agente AI genera codice, deve anche produrre una dimostrazione in PROOF.bend che l'implementazione soddisfi tali leggi. Il type checker di Bend verifica quindi la dimostrazione, fungendo da gatekeeper matematico.

"'Non fare errori' ora è type-checked," spiega il sito web del progetto. Il sistema è basato su una teoria dei tipi dipendenti affine chiamata BendTT, con un runtime parallelo (BendRT) che esegue il codice verificato.

Dimostrazione nel Mondo Reale: Un Gioco Impossibile da Barare

Il progetto dimostra il concetto con un semplice gioco. Una legge dichiara che vincere è impossibile: nessuna sequenza di mosse può portare alla vittoria. Quando una richiesta di funzionalità di test chiede all'AI di "far avvolgere la scacchiera", il sistema o rifiuta la modifica se viola la legge o costringe l'AI a riprovare finché non può dimostrare che il nuovo comportamento mantiene ancora l'invariante.

Senza Bend, un tale bug verrebbe integrato silenziosamente. Con Bend, integrare una violazione è matematicamente impossibile—è un teorema, non solo un test.

Prestazioni: Velocità C, Parallelismo GPU

Bend non riguarda solo la correttezza. Compila in codice nativo che gira quasi veloce come il C su un singolo core, mentre lo stesso binario può scalare automaticamente a sedici core o migliaia di core GPU. I benchmark su un Apple M4 Max mostrano Bend superare il C su carichi di lavoro paralleli, con l'azienda che afferma fino a 100x di accelerazione rispetto all'esecuzione su singolo core sulle GPU.

La magia risiede nelle reti di interazione, un modello computazionale che suddivide il lavoro in chiamate ricorsive binarie che possono essere distribuite sull'hardware senza threading esplicito, lock o codice kernel. Il runtime gestisce automaticamente allocazione, garbage collection e scheduling.

Compilazione Veloce per l'Iterazione dell'AI

I tradizionali checker di dimostrazioni come Lean o Rocq possono impiegare minuti su codebase di medie dimensioni—troppo lenti per agenti AI che devono iterare rapidamente. Il type checker di Bend completa in meno di un secondo, rendendolo pratico per l'AI per verificare ogni modifica. Questa velocità è cruciale per integrare il controllo delle dimostrazioni nel ciclo di sviluppo.

Bend2 e l'Evoluzione del Runtime

Il progetto si è evoluto rapidamente. Bend2 ha come target HVM4, la quarta generazione di una linea di runtime iniziata nel 2022. Una tappa notevole è avvenuta nel luglio 2026, quando un modello di codifica (Fable di Anthropic) ha implementato il runtime CUDA durante la notte da una versione Metal di riferimento, funzionando apparentemente più velocemente di Metal su hardware RTX—circa 10x parallelo C per la maggior parte dei programmi.

Questo successo di porting sottolinea una tesi chiave: i compiti di ingegneria ben specificati possono essere automatizzati, ma i livelli di progettazione e verifica rimangono umani.

Come Iniziare

L'installazione è semplice:

curl -fsSL https://bend-lang.com/install.sh | sh

Aggiungi bend guide, LAWS.bend e bend PROOF.bend al tuo file AGENTS.md, quindi istruisci la tua AI a "usare Bend." Il linguaggio funziona meglio su Linux e macOS per lo sviluppo back-end.

Perché è Importante

Bend rappresenta una scommessa significativa sul futuro dello sviluppo software. Mentre gli agenti AI scrivono più codice, la capacità di verificare formalmente che il loro output soddisfi le specifiche diventa critica. Rendendo la correttezza dimostrabile e il parallelismo automatico, Bend offre una visione convincente: codice che è sia veloce che affidabile, anche quando nessun umano lo ha letto.

Il progetto è ancora giovane e in evoluzione, con l'autore che riconosce che è un lavoro in corso. Ma la combinazione di controllo delle dimostrazioni, parallelismo automatico e design favorevole all'AI posiziona Bend come un linguaggio da tenere d'occhio per i team che abbracciano lo sviluppo assistito dall'AI.