Leslie Lamport, vincitore del premio Turing per i contributi nello studio dell'affidabilità e della consistenza dei sistemi di calcolo, è stato pioniere nel campo teorico e pratico dei sistemi distribuiti e concorrenti in cui più componenti su reti diverse si coordinano per raggiungere un obiettivo comune. Da internet al cloud computing, dal machine learning all'intelligenza artificiale.
All'inizio degli anni '80, Lamport creò anche LaTeX (da leggere come latek, la X è infatti la lettera greca chi), un linguaggio di markup per la preparazione di testi che fornisce modi sofisticati per comporre formule complesse e formattare documenti scientifici.
Nel 1989, Lamport ha inventato Paxos, un "algoritmo di consenso" che consente a più computer di eseguire compiti complessi; senza di esso, l'informatica moderna non potrebbe esistere. Ha anche portato maggiore attenzione su una serie di problemi matematici, dando loro nomi distintivi come l'algoritmo della panetteria e il problema dei generali bizantini.
Il lavoro di Lamport dagli anni '90 si è concentrato sulla verifica formale, l'uso di prove matematiche per verificare la correttezza dei sistemi software e hardware. In particolare, ha creato un linguaggio di specifica chiamato TLA+ (per la logica temporale delle azioni), che utilizza il linguaggio preciso della matematica per prevenire bug ed evitare difetti di progettazione.
LEGGI ALTRO...