I see that Leslie Lamport (a "Principal Researcher at Microsoft
Research") has won the 2013 Turing award. The announcement that I saw on
the LaTeX3 mailing list includes the paragraph:
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. His notions
of safety, where nothing bad happens, and liveness, where something good
happens, contribute to the reliability and robustness of software and
hardware engineering design. His solutions for Byzantine Fault Tolerance
contribute to failure prevention in a system component that behaves
erroneously when interacting with other components. His creation of
temporal logic language (TLA+) helps to write precise, sound
specifications. He also developed LaTeX, a document preparation system
that is the de facto standard for technical publishing in computer
science and other fields.
After some of the discussions about parsing LaTeX (e.g. for round trips)
on the LyX lists I confess this sounded like a spoof to me, but it does
seem to be genuine (and worth $250 000).
Andrew
