Escaping the Quicksand: A Call to Arms

Immaginate un mondo in cui l'invisibile ingranaggio della vita moderna — le nostre banche, gli ospedali, le reti elettriche e le reti di comunicazione — è costruito su una fondamenta che sta lentamente affondando. Questa è la realtà che l'industria informatica affronta oggi. Per decenni, il modo standard di costruire il software è stato quello di scrivere una descrizione approssimativa di ciò che un programma dovrebbe fare, poi scrivere il codice e infine testarlo eseguendolo con vari input per vedere se si rompe. Questo metodo, noto come sviluppo "test-and-debug", ha permesso alla tecnologia di fiorire, ma lascia i sistemi ricchi di difetti nascosti. Poiché le descrizioni originali sono spesso vaghe e scritte in linguaggio ordinario, non possono essere controllate dalle macchine, e poiché il testing può coprire solo una minuscola frazione dei miliardi di possibili modi in cui un programma potrebbe comportarsi, molti errori sfuggono. Con l'intelligenza artificiale che inizia a scrivere più codice, questo ciclo minaccia di accelerare, creando nuovi sistemi vasti, ancora più complessi e fragili di prima, costruiti su una "quicksand" (sabbia mobile) di scelte progettuali vecchie di decenni, fatte quando gli attacchi informatici erano rari e la potenza di calcolo scarsa.

Due ricercatori, Peter Sewell dell'Università di Cambridge e Jean Pichon-Pharabod dell'Università di Aarhus, sostengono che l'industia sia bloccata in un ciclo pericoloso da settantacinque anni. Osservano che, mentre siamo diventati incredibilmente esperti nello scrivere codice, abbiamo trascurato le definizioni precise di ciò che quel codice dovrebbe ottenere. L'approccio attuale si basa su specifiche in prosa: paragrafi di testo che descrivono il comportamento di un sistema. Sebbene questi siano facili da leggere per gli esseri umani, sono intrinsecamente ambigui e incompleti. Un lettore umano potrebbe interpretare una frase in un modo, mentre una macchina o un altro essere umano la interpreta diversamente. Poiché queste descrizioni non possono essere testate direttamente da un computer, gli sviluppatori sono costretti a indovinare quale debba essere il comportamento corretto, ricorrendo spesso a controlli semplici come "il programma va in crash?" piuttosto che verificare se il programma stia effettivamente facendo la cosa giusta. Questo divario tra l'intento scritto e il codice effettivo crea un enorme debito tecnico, un costo nascosto che si manifesta come vulnerabilità di sicurezza e guasti del sistema che possono essere sfruttati dagli attaccanti.

Gli autori suggeriscono che la soluzione non sia abbandonare i test, ma cambiare il modo in cui utilizziamo le specifiche. Inveve di scrivere paragrafi vaghi, propongono di creare specifiche che siano eseguibili, ovvero scritte in una forma che un computer possa eseguire. Immaginate una specifica che agisca come un arbitro dal vivo durante il processo di sviluppo. Mentre il codice viene scritto o generato, questa specifica eseguibile gira accanto ad esso, controllando istantaneamente se il comportamento del codice corrisponde alle regole previste. Se il codice tenta di fare qualcosa che la specifica proibisce, il sistema lo segnala immediatamente. Questo crea un ciclo di feedback molto più stretto, permettendo agli sviluppatori di individuare gli errori man mano che si verificano, anziché settimane dopo. Questo approccio può essere applicato in diversi modi: si può partire dal codice e scrivere una specifica per corrispondergli, partire da una specifica e generare codice che si adatti ad essa, oppure costruire entrambi insieme. La chiave è che la specifica non sia solo un documento da leggere, ma uno strumento da usare.

Tuttavia, i ricercatori riconoscono che non si tratta di un semplice interruttore da attivare. Per far sì che ciò funzioni su scala massiccia, la comunità informatica deve costruire un nuovo livello di infrastruttura. Attualmente, non esistono definizioni universalmente accettate e leggibili dalle macchine per il comportamento di molte tecnologie fondamentali, come il linguaggio di programmazione C, il linguaggio Rust o le istruzioni che eseguono i chip dei computer. Sebbene alcuni ricercatori abbiano creato con successo queste definizioni per parti specifiche del sistema, non esiste un quadro unificato che le connetta tutte. Gli autori sottolineano che costruire questa infrastruttura è una sfida di scala e cooperazione. Richiede uno sforzo massiccio e coordinato da parte di università, governi e aziende tecnologiche per creare, validare e mantenere queste definizioni precise per l'intero stack tecnologico, dall'hardware fino ai servizi cloud.

Il documento affronta anche il ruolo dell'intelligenza artificiale. Gli autori avvertono che usare semplicemente l'IA per scrivere più codice senza questi migliori cicli di feedback non farà altro che peggiorare il problema. L'IA può generare codice più velocemente degli esseri umani, ma se quel codice è costruito su fondamenta traballanti e testato solo con i vecchi metodi inefficaci, creerà semplicemente sistemi più grandi con più errori nascosti. Al contrario, se l'IA viene utilizzata per aiutare a generare e controllare queste specifiche eseguibili, potrebbe diventare uno strumento potente per migliorare la qualità del software. Gli autori immaginano un futuro in cui l'IA aiuti a creare specifiche rigorose, e dove quelle specifiche vengano utilizzate per verificare che sia il codice scritto dagli umani sia quello generato dall'IA sia corretto. Ciò permetterebbe un aumento graduale della fiducia, partendo da test semplici per arrivare a più complessi processi matematici di correttezza, il tutto senza richiedere che ogni sviluppatore diventi un matematico.

Nonostante il percorso chiaro, gli autori sostengono che l'industria sia stata frenata da un disallineamento di incentivi. Le aziende tecnologiche sono motivate a rilasciare prodotti rapidamente per catturare quote di mercato, mentre i rischi di fallimento ricadono in gran parte sulla società e sugli utenti finali. Costruire l'infrastruttura robusta necessaria per prevenire questi fallimenti è costoso e richiede tempo, e nessuna singola azienda vuole farsi carico dell'intero costo di risoluzione di problemi che interessano tutti. I ricercatori chiedono un impegno collettivo, simile ai grandi progetti visti nella fisica o nella biologia, per finanziare e coordinare la creazione di questa infrastruttura semantica. Suggeriscono che, sebbene il costo sia significativo, esso è una frazione minima delle attuali spese per l'intelligenza artificiale ed è essenziale per garantire il futuro dell'informatica. Senza questo cambiamento, l'industria rimane intrappolata in un ciclo di costruzione di sistemi sempre più complessi su fondamenta troppo deboli per sostenerli, lasciando la società vulnerabile a un rischio costante.

Gli autori concludono che gli strumenti e i metodi per risolvere questo problema esistono già. I ricercatori hanno dimostrato con successo come definire il comportamento di sistemi complessi e verificarli con un alto grado di fiducia. Ciò che manca è la volontà di portare questi metodi nella pratica quotidiana e di costruire l'infrastruttura condivisa che li renda accessibili a tutti. Il documento funge da appello all'azione per la comunità di ricerca, i leader dell'industria e le agenzie di finanziamento affinché collaborino a questo compito. Passando da descrizioni vaghe verso specifiche precise ed eseguibili, il mondo informatico può sfuggire alla sabbia mobile del debito tecnico e costruire un futuro che sia non solo più innovativo, ma anche fondamentalmente più sicuro e affidabile.