Wednesday, November 12, 2014 - 4:00pm to Thursday, November 13, 2014 - 3:55pm
Event Calendar Category
CSAIL
Speaker Name
Leslie Lamport
Building and Room number
32-123
Abstract
Architects draw detailed plans before construction begins. Software
engineers don't. Can this be why buildings seldom collapse and
programs often crash? A blueprint for software is called a
specification. TLA+ specifications have been described as exhaustively
testable pseudo-code. High-level TLA+ specifications can catch design
errors that are now found only by examining the rubble after a system
has collapsed.
Biography
Dr. Lamport received a doctorate in mathematics from Brandeis
University, with a dissertation on singularities in analytic partial
differential equations. This, together with a complete lack of
education in computer science, prepared him for a career as a computer
scientist at Massachusetts Computer Associates, SRI, Digital, and
Compaq. He claims that it is through no fault of his that of those
four corporations, only the one that was supposed to be non-profit
still exists. He joined Microsoft in 2001, but that company has not
yet succumbed.
Dr. Lamport's initial research in concurrent algorithms made him
well-known as the author of LaTeX, a document formatting system for
the ever-diminishing class of people who write formulas instead of
drawing pictures. He is also known for writing
"A distributed system is one in which the failure of a computer you
didn't even know existed can render your own computer unusable." which
established him as an expert on distributed systems. His interest in
Mediterranean history, including research on Byzantine generals and
the mythical Greek island of Paxos, led to his receiving five honorary
doctorates from European universities, and to the IEEE sending him to
Italy to receive its 2004 Piore Award and to Quebec to receive its
2008 von Neumann medal. However, he has always returned to his home in
California. This display of patriotism was rewarded with membership in
the National Academy of Engineering and the National Academy of
Sciences.
More recently, Dr. Lamport has been annoying computer scientists and
engineers by urging them to understand an algorithm or system before
implementing it, and scaring them by saying they should use
mathematics. In an attempt to get him to talk about other things, the
ACM gave him the 2013 Turing Award.