Bend: il linguaggio che vuole dimostrare che il codice scritto dall'AI è corretto

Il meccanismo proposto da Bend si basa su un file, chiamato LAWS.bend, dove dichiari invarianti che il tuo programma deve rispettare sempre, qualunque modifica venga fatta in futuro. Un esempio citato dagli autori è un gioco da tavolo: la legge "nessuna sequenza di mosse porta alla vittoria" (per verificare che il motore del gioco sia davvero imbattibile). Quando chiedi a un assistente AI di aggiungere una funzione — ad esempio far sì che la board "avvolga" i bordi — il compilatore richiede una prova scritta che dimostri che quella modifica non rompe la legge dichiarata. Se la prova non regge, il codice non compila: non è una revisione umana che può essere distratta o affrettata, è un controllo meccanico che non si stanca mai e non fa eccezioni.

Il dettaglio tecnico che rende l'idea praticabile, e non solo accademica, è la velocità: il type checker di Bend funziona da dimostratore di teoremi (come in linguaggi accademici quali Lean o Rocq), ma dove quelli impiegano minuti su una codebase di medie dimensioni, Bend punta a farlo in un secondo o meno. È la differenza tra un controllo che un umano fa una volta prima del rilascio e un controllo che un agente AI può rieseguire dopo ogni singola modifica che propone, senza rallentare il ciclo di lavoro.

Il problema che Bend prova a risolvere esiste indipendentemente dal linguaggio: quando un assistente AI genera codice più in fretta di quanto un umano possa rileggerlo con attenzione, il collo di bottiglia si sposta dalla scrittura alla verifica. La risposta pratica, oggi, per chi lavora con Python, TypeScript o qualunque altro linguaggio mainstream, è la stessa in sostanza: rendere espliciti, in una forma che una macchina può controllare, gli invarianti che non devono mai rompersi — tramite tipi più stringenti, asserzioni a runtime, test di proprietà (property-based testing) invece di soli esempi singoli, e contratti espliciti sulle funzioni critiche. Non è una prova formale in senso matematico, ma il principio è identico: non fidarti della lettura umana come unico controllo quando il volume di codice generato cresce più in fretta della tua capacità di rileggerlo riga per riga.

C'è anche un parallelo pratico con una tendenza che si vede sempre più spesso negli strumenti di coding agentico: un file AGENTS.md o equivalente, letto automaticamente dall'assistente, che raccoglie le regole del progetto. Bend spinge quell'idea un passo oltre: non basta scrivere la regola in prosa sperando che l'AI la rispetti, la regola diventa un teorema che il compilatore verifica.

Bend è un progetto giovane: gli stessi autori avvisano di aspettarsi bug e di segnalarli, e consigliano di usarlo soprattutto sul backend, su Linux o macOS, non ancora come sostituto universale del tuo stack attuale. È il tipo di strumento da guardare con curiosità e da provare su un progetto piccolo o personale prima ancora di pensare a portarlo in produzione — ma l'idea che porta con sé, "le regole importanti vanno rese verificabili meccanicamente, non solo scritte in un commento o in un documento che l'AI potrebbe ignorare", è già utile oggi, qualunque sia il linguaggio con cui lavori.