The Pulse
Bend usa leggi e dimostrazioni per impedire errori di programmazione dell’IA
Bend presenta un linguaggio di programmazione che consente agli sviluppatori di definire regole importanti in LAWS.bend e richiede dimostrazioni prima che il codice scritto dall’IA venga sottoposto a commit. Il progetto combina una sintassi
AI.info Team ·
Bend pone un controllo basato su dimostrazioni tra una modifica dell’IA e un programma in esecuzione
Bend è un linguaggio di programmazione pensato 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 dovrebbero valere sempre. Il progetto abbina queste leggi a dimostrazioni e chiede agli utenti di eseguire bend PROOF.bend prima di effettuare il commit delle modifiche.
Il sito descrive l’obiettivo in termini diretti: i prompt in linguaggio naturale possono essere ambigui, mentre le leggi forniscono all’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 sulla base di affermazioni formali, anziché affidarsi soltanto a una persona che legga ogni riga generata.
LAWS.bend trasforma i requisiti in affermazioni verificate
La dimostrazione di Bend usa un gioco con una legge secondo cui nessuna sequenza di mosse può portare a uno stato vincente. L’esempio mostra un agente di IA a cui viene chiesto di fare in modo che la scacchiera riparta dai bordi opposti. Senza la legge, dice il sito, l’errore che ne risulta può essere integrato nel codice. Con LAWS.bend al suo posto, l’agente deve riprovare finché non produce un’implementazione e una dimostrazione che rispettino la regola dichiarata.
La legge d’esempio quantifica una sequenza di mosse, ripercorre quelle mosse a partire dalla posizione iniziale e controlla che la scacchiera risultante non sia uno stato vincente. Il file PROOF.bend associato definisce una dimostrazione della legge. Bend descrive questa struttura come un’istruzione AGENTS.md supportata da una dimostrazione: lo sviluppatore registra ciò che non deve essere compromesso e il processo di verifica impedisce che venga approvato codice che viola il requisito.
Le istruzioni di configurazione del progetto dicono agli agenti di usare LAWS.bend per le regole importanti e di eseguire bend PROOF.bend prima di effettuare il commit. Chiedono inoltre agli agenti di parallelizzare il codice ogni volta che è possibile. Il sistema non decide quali requisiti siano importanti: spetta agli sviluppatori individuare il comportamento che vogliono proteggere ed esprimerlo sotto forma di legge.
Un linguaggio veloce con esecuzione nativa e parallela
Bend si descrive come un linguaggio veloce, con la sintassi di Python, la velocità del C, il parallelismo di CUDA e dimostrazioni in stile Lean. Il suo compilatore genera codice nativo. Il sito afferma che un programma può essere eseguito su un singolo core a una velocità vicina a quella del C, mentre lo stesso binario può essere eseguito anche su sedici core della CPU o su una GPU.
Il suo modello di parallelismo si basa sulla suddivisione del lavoro in chiamate che Bend distribuisce tra i core disponibili, prima di riunire i risultati. Il progetto afferma che così i programmatori non devono scrivere thread, lock o kernel GPU. Una dimostrazione esegue un programma pow2.bend su 4.096 core GPU.
Bend presenta inoltre il proprio verificatore dei tipi come un verificatore di dimostrazioni, paragonabile per scopo ai verificatori usati da Lean e Rocq. Secondo il sito, questi sistemi possono impiegare minuti su una codebase di medie dimensioni, mentre Bend è progettato per completare le verifiche in non più di un secondo. L’obiettivo dichiarato è consentire a un agente di IA di verificare il proprio lavoro dopo ogni modifica.
Un progetto giovane rivolto allo sviluppo assistito dall’IA
Le istruzioni di installazione di Bend forniscono un comando da shell per installare il linguaggio e consigliano Linux e macOS per un’esperienza ottimale. Il sito afferma che Bend funziona meglio nel backend e invita gli utenti a segnalare i problemi, perché il progetto è ancora in evoluzione.
Il progetto rimanda a una guida al linguaggio, a un articolo sulla teoria dei tipi dipendenti affini di Bend e a un articolo sul suo runtime parallelo per CPU e GPU. Avverte inoltre gli utenti di aspettarsi dei bug. La promessa centrale di Bend è quindi circoscritta ma precisa: quando uno sviluppatore dichiara una regola importante e fornisce una dimostrazione valida, il verificatore può bloccare una modifica generata dall’IA che infrange quella regola. L’utilità del processo dipende dal fatto che le leggi dichiarate descrivano accuratamente il comportamento richiesto dall’applicazione.