GCi sono due tipi di persone che hanno buone ragioni per essere grati a Tony Hoare: in primo luogo, tutti coloro che ripongono ancora le proprie speranze nei computer, e in secondo luogo, tutti coloro che ora odiano cose come la peste. Gli exploit di Hoare rientrano in quattro aree altamente specializzate: a) ordinamento dei dati, b) verifica formale del programma, c) sistemi concorrenti e infine d) teoria assiomatica della programmazione. Ma tutti i suoi successi individuali derivano dalla perseveranza senza compromessi di questo pensatore nella sua convinzione che non ci si dovrebbe avvicinare all'informatica come un pazzo che si lascia attirare su un nuovo tipo di aereo di cui nemmeno il pilota capisce come funziona. . Solo perché è veloce.

Charles Anthony Richard Hoare, nato a Colombo nel 1934, figlio di un funzionario coloniale britannico e figlia di un piantatore di tè, e che fu elevato al rango nobiliare dalla regina Elisabetta II all'inizio del millennio per i suoi servizi al pensiero computazionale, univa quattro professioni che raramente collaboravano: è apprendista, filologo classico, esperto del pensiero antico, oltre che filosofo e matematico. Dopo essersi laureato in archeologia nel 1956, imparò il russo alla Marina, studiò informatica a Oxford e poi si recò a Mosca, dove ebbe la fortuna di studiare con Andrei Nikolayevich Kolmogorov, uno dei matematici più importanti della Russia. L'era moderna. La classificazione di Kolmogoro si basa su diversi tipi di ricerca di base; La sua semplificazione della teoria della probabilità nel 1933 fu particolarmente importante, confrontando i fondamenti della geometria di Euclide utilizzando i presupposti più semplici (“Se A e B sono uguali a C, allora sono anche uguali” e simili). Kolmogorov aveva bisogno solo di tre assiomi per giustificare le probabilità: 1.) Le probabilità sono definite come numeri reali positivi, 2.) Almeno un evento nello spazio delle probabilità ha probabilità 1 ed è quindi certo. 3.) Per due eventi incompatibili, la probabilità che si verifichi una di queste due cose è uguale alla somma delle singole probabilità.

Al ritorno da Mosca, Hoare, allievo di Kolmogorov, si elevò per la prima volta in Inghilterra dall'aria rarefatta della massima astrazione alle presunte profondità della pratica di programmazione e inventò all'inizio degli anni '60 l'algoritmo Quicksort, che continua a garantire l'ordine (e non solo scientifico) nelle nuove scienze. , versioni migliorate fino ad oggi. “So come si fa, ma non so spiegarlo”: questo slogan poteva anche funzionare, ma Hoare, invece, voleva subito assicurarsi che il nuovo software in fase di test non passasse troppe volte. E per molto tempo, finché ogni dubbio sul suo valore non svanirà. Questa pratica di test è utilizzata ancora oggi; Tuttavia, Hoare obiettò, dicendo che un teorema matematico non poteva essere dimostrato introducendo le prime migliaia di numeri naturali e alla fine ottenendone abbastanza, ma seguendo tutti i passaggi dagli assiomi non falsificabili al teorema (Euclide e Kolmogorov annuirono in accordo).

Come i filosofi e la pasta

La “verifica formale” dei programmi basati su questo è stata la sua principale preoccupazione pratica sin dalla prima circolare di Hoare, simile a un manifesto, nel 1967. Quanta negligenza, abilità e confusione abbia fatto vergognare o addirittura impedire si può solo immaginare. Non gli era affatto chiaro che lo sforzo di semplificazione che le sue idee richiedevano nella suddivisione dei compiti informatici fosse in tensione con la complessità della loro realtà quotidiana. Uno dei tipici momenti di esasperazione in questo campo è la sincronicità che è sempre legata a qualcosa per cui Hoare e il collega Edsger Dijkstra hanno creato la bellissima parabola sui filosofi e la pasta.