Due modi di costruire un sistema, in memoria di Tony Hoare
Ha passato la vita a dimostrare che il primo metodo è possibile. Il mondo ha scelto il secondo.
«Ci sono due modi di progettare un sistema software: il primo è farlo così semplice da essere palesemente privo di difetti, il secondo è farlo così complicato da non avere difetti evidenti. Il primo metodo è molto più difficile.»
Questa è una frase di Tony Hoare pronunciata a Nashville il 27 ottobre 1980, nella lectio per il Turing Award intitolata The Emperor's Old Clothes. La si trova ovunque: diapositive, firme email, conferenze, quasi sempre senza contesto. Il contesto è che la persona che l'ha pronunciata ha passato i successivi quarant'anni a cercare di rendere il primo metodo praticabile. Hoare è morto il 5 marzo 2026 a Cambridge, a 92 anni.
Il suo percorso non era quello di un informatico. Aveva studiato lettere classiche e filosofia a Oxford, seguendo un programma chiamato Greats, quello con Virgilio e Platone. Ha imparato il russo durante il servizio militare in marina. Nel 1959, con una borsa del British Council, è finito a Mosca come studente nel dipartimento di teoria della probabilità di Andrej Kolmogorov, tra i fondatori della probabilità moderna. Un'offerta del National Physical Laboratory lo ha dirottato sulla traduzione automatica dal russo — così, tra guerra fredda e linguistica computazionale, un classicista britannico a Mosca ha inventato Quicksort.
Si tratta di un algoritmo di ordinamento: scegli un elemento da una lista, metti tutto quello che è più piccolo a sinistra e tutto quello che è più grande a destra, poi ripeti su ciascuna metà fino a che la lista è in ordine. Gli serviva per ordinare alfabeticamente le parole da tradurre, perché il dizionario era su nastro magnetico e una sola passata richiedeva l'ordine giusto. L'algoritmo che ha scritto a 25 anni è ancora oggi tra i più usati al mondo.
Dieci anni dopo, nel 1969, ha pubblicato An Axiomatic Basis for Computer Programming. È il paper che fonda la Hoare Logic. Normalmente, per sapere se un programma funziona, lo testi. Lo fai girare con degli input, controlli gli output, e speri di aver coperto abbastanza casi. Hoare propone un'alternativa: dimostrarlo. Per ogni pezzo di codice, scrivi cosa deve essere vero prima dell'esecuzione (precondizione) e cosa deve essere vero dopo (postcondizione). Se riesci a dimostrare che il codice trasforma sempre la prima nella seconda, non stai testando che il programma funzioni. Stai dimostrando che non può fare altro.
Un esempio. Vuoi scambiare il valore di due variabili, X e Y. Il codice usa tre righe e una variabile d'appoggio: copia X da parte, metti Y al posto di X, rimetti il valore originale in Y. Prima dell'esecuzione, X vale x e Y vale y; dopo, X vale y e Y vale x. La dimostrazione di Hoare ripercorre queste tre istruzioni al contrario, verificando passo per passo che le variabili tornino esattamente alla situazione di partenza. Non per un caso o per mille: per ogni possibile coppia di valori.
Con tre istruzioni la cosa è gestibile. Hoare lo sapeva, e l'ha costruita per scalare: la logica include regole per la composizione sequenziale (se dimostri i pezzi, dimostri l'insieme), per le condizioni (if/then/else), per i cicli (dove serve trovare un'invariante, una proprietà che resta vera a ogni iterazione). L'idea era che la dimostrazione avesse la stessa struttura del programma: componi le prove come componi il codice.
La differenza rispetto ai test non è di grado. I test trovano gli errori che hai pensato di cercare: quelli per cui hai scritto un test, quelli che ti sono venuti in mente, quelli scoperti dopo un crash in produzione. La verifica formale esclude tutti gli altri.
Qualcuno l'ha fatto davvero. seL4 è un microkernel, il cuore minimo di un sistema operativo, di 8.700 righe di codice C. Un team australiano ha impiegato vent'anni di lavoro cumulativo per dimostrare formalmente che ogni riga fa esattamente ciò che la specifica dice. Nessun buffer overflow, crash o comportamenti imprevisti: non perché testato, ma perché dimostrato. CompCert è un compilatore C verificato: il codice macchina che produce è dimostrato identico nel comportamento al sorgente. Quando i ricercatori di Csmith hanno cercato sistematicamente bug in tutti i compilatori C esistenti, CompCert è stato l'unico in cui non ne hanno trovati.
Però seL4 è fatto di 8.700 righe. Un browser moderno ne ha decine di milioni. Il costo della verifica formale cresce con il numero di stati possibili del sistema, e i programmi reali ne hanno miliardi. Quindi si applica a componenti piccoli con requisiti estremi: microkernel, compilatori, protocolli crittografici, software aerospaziale. Tutto il resto viene rilasciato con la speranza ragionevole che i test coprano abbastanza casi.
Hoare lo sapeva. E nel 2009, alla conferenza QCon London, ha fatto qualcosa di raro per un vincitore del Turing Award: ha ammesso un errore. Nel 1965, progettando il sistema di tipi di ALGOL W, aveva introdotto il riferimento null, «semplicemente perché era così facile da implementare». L'ha chiamato il suo errore da un miliardo di dollari. Non stava esagerando: i null reference sono ancora oggi tra le cause più comuni di crash nel software. Linguaggi recenti come Rust, Kotlin e Swift hanno sistemi di tipi che li escludono a livello di compilatore, strumenti che esistono perché Hoare ha detto in pubblico dove aveva sbagliato.
Ha passato la vita a dimostrare che il primo metodo è possibile, e ha ammesso in pubblico i propri errori. Il mondo ha scelto il secondo — non perché avesse torto, ma perché il primo costa troppo.