"Lamport's practical and widely used algorithms and tools have applications in security, cloud computing, embedded systems and database systems as well as mission-critical computer systems that rely on secure information sharing and interoperability to prevent failure."
Many probably think of him mainly as the initial developer of LaTeX, for which I am often personally grateful, but his contributions go far beyond this. Have a look at
and form your own conclusions.
During the Ballmer era of Microsoft, there was much heat and noise related to claims that Linux could not innovate. Yet Turing award winners associated with Microsoft were a bit thin on the ground. Not absent: Charles P. Thacker won in 2009, and one of his many accomplishments was helping to establish Microsoft Research Cambridge in Cambridge, England.
Those days are hopefully behind us; it was mostly strategic corporate marketing noise. Microsoft has been been funding his work, by the simple means of employing him, since 2001. Microsoft deserves our thanks as well.