The Pulse

Bend usa leggi e dimostrazioni per bloccare gli errori di programmazione dell’IA

Bend presenta un linguaggio di programmazione che consente agli sviluppatori di dichiarare regole importanti in LAWS.bend e richiedere dimostrazioni prima che il codice scritto dall’IA venga sottoposto a commit. Il progetto combina una sint

AI.info Team · Scritto con l’IA · verificato · 2026-09-19

Bend introduce un controllo basato su dimostrazioni tra una modifica dell’IA e l’esecuzione del programma

Bend è un linguaggio di programmazione progettato per limitare gli errori nel software scritto con agenti di IA. Il suo meccanismo centrale è LAWS.bend, un file in cui gli sviluppatori dichiarano regole che devono essere sempre rispettate. Il progetto associa a queste leggi delle dimostrazioni e chiede agli utenti di eseguire bend PROOF.bend prima di sottoporre le modifiche a commit.

Il sito descrive l’obiettivo in termini diretti: i prompt in linguaggio naturale possono essere ambigui, mentre le leggi forniscono a un’IA una specifica più precisa del comportamento desiderato. Le dimostrazioni verificano poi se l’implementazione soddisfa i requisiti dichiarati. Bend presenta questo processo come un modo per esaminare il codice attraverso affermazioni formali, invece di affidarsi soltanto a una persona che legga ogni riga generata.

LAWS.bend trasforma i requisiti in affermazioni verificabili

La dimostrazione di Bend usa un gioco con una legge secondo cui nessuna sequenza di mosse può produrre uno stato vincente. Nell’esempio, a un agente di IA viene chiesto di fare in modo che il tabellone si richiuda su sé stesso. Senza la legge, afferma il sito, la modifica che contiene l’errore può essere integrata. Con LAWS.bend in uso, l’agente deve riprovare finché non produce un’implementazione e una dimostrazione che preservino la regola dichiarata.

La legge dell’esempio quantifica su una sequenza di mosse, ripete quelle mosse a partire dalla posizione iniziale e verifica che il tabellone risultante non sia in uno stato vincente. Il file associato PROOF.bend definisce una dimostrazione per la legge. Bend descrive questo meccanismo come un’istruzione in AGENTS.md supportata da una dimostrazione: lo sviluppatore registra ciò che non deve essere compromesso e il processo di verifica impedisce che il codice che viola quel requisito superi il controllo.

Le istruzioni di configurazione del progetto indicano agli agenti di usare LAWS.bend per le regole importanti e di eseguire bend PROOF.bend prima del commit. Chiedono inoltre agli agenti di parallelizzare il codice ogni volta che sia possibile. Il sistema non decide quali requisiti siano importanti: gli sviluppatori devono individuare il comportamento che vogliono proteggere ed esprimerlo come legge.

Un linguaggio veloce con esecuzione nativa e parallela

Bend si descrive come un linguaggio veloce, con la sintassi di Python, la velocità di C, il parallelismo di CUDA e dimostrazioni in stile Lean. Il suo compilatore produce codice nativo. Secondo il sito, un programma può essere eseguito su un solo core a una velocità vicina a quella di C, mentre lo stesso binario può essere eseguito anche su sedici core di CPU o su una GPU.

Il suo modello parallelo si basa sulla suddivisione del lavoro in chiamate che Bend distribuisce tra i core disponibili prima di riunire i risultati. Secondo il progetto, questo evita ai programmatori di dover scrivere thread, lock o kernel GPU. Una dimostrazione esegue un programma pow2.bend su 4096 core di GPU.

Bend presenta inoltre il suo verificatore di tipi come un verificatore di dimostrazioni, con una funzione paragonabile a quella dei verificatori usati da Lean e Rocq. Secondo il sito, questi sistemi possono impiegare minuti su una base di codice di medie dimensioni, mentre Bend è progettato per completare le verifiche in al massimo un secondo. L’obiettivo dichiarato è consentire a un agente di IA di controllare il proprio lavoro dopo ogni modifica.

Un progetto giovane rivolto allo sviluppo assistito dall’IA

Le istruzioni di installazione di Bend forniscono un comando di shell per installare il linguaggio e raccomandano Linux e macOS per un’esperienza ottimale. Il sito afferma che Bend funziona meglio nel back end e chiede agli utenti di segnalare i problemi, perché il progetto è ancora in evoluzione.

Il progetto rimanda a una guida al linguaggio, a un paper sulla teoria dei tipi dipendenti affini di Bend e a un paper sul suo runtime parallelo per CPU e GPU. Avverte inoltre gli utenti di aspettarsi bug. La promessa centrale di Bend è dunque limitata ma specifica: quando uno sviluppatore dichiara una regola importante e fornisce una dimostrazione valida, il verificatore può bloccare una modifica generata dall’IA che viola quella regola. L’utilità del processo dipende dal fatto che le leggi dichiarate descrivano accuratamente il comportamento di cui l’applicazione ha bisogno.