Tony Hoare
Nel 1960 iventò l'algoritmo di ordinamento più usato al mondo: è un algoritmo che viene utilizzato per elencare gli elementi di un insieme secondo una sequenza stabilita da una relazione d'ordine i elemento sia minore (o maggiore) di quello che lo segue. In assenza di altre specifiche, la relazione d'ordine viene sempre considerata totale (cioè tale da rendere sempre possibile il confronto tra due elementi dell'insieme): le relazioni d'ordine parziale danno origine agli algoritmi di ordinamento topologico. A seconda del verso della relazione considerato, un ordinamento può essere ascendente o discendente.
Egli ha anche sviluppato le logiche di Hoare, la correttezza dei programmi, e il linguaggio formale Comunicating Sequential Prosesse
è un sistema formale che rientra tra le semantiche assiomatiche pubblicato per la prima volta nel 1969 da che si prefigge, definendo un insieme iniziale di assiomi e di regole su di essi, di valutare la cortezza di programmi utilizzando il rigore dei formalismi matematici.
La logica è stata sviluppata per essere utilizzata con un semplice linguaggio di programmazione imperativo ed ha subito sviluppi ulteriori per merito dello stesso Hoare e di altri ricercatori per la gestione di casistiche particolari quali la concorrenza, i puntatori e le procedure.
I linguaggi si dividono in:
linguaggio naturale: Un linguaggio naturale è il linguaggio utilizzato normalmente e naturalmente da un soggetto come l'italiono può essere per noi
linguaggio formale: E' il linguaggio che si usa per esempio per scrivere programmi su computer, come lo può essere html. In fatti la grossa differenza tra questo linguaggio e il precedente è il fatto che un linguaggio formale non può che essere interpretato che in un modo, non lascia quindi ambiguità.