Leslie Lamport, Microsoft Research

Thursday, June 28, 2012 18:00
Amphi 25, Sorbonne University - Faculté des Sciences

What is Computation?

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. Among his other contributions is the TLA+ specification language, which represents a Quixotic attempt to overcome computer scientists' antipathy towards mathematics. Despite having received five honorary doctorates from European universities and having been sent by the IEEE to Italy to receive its 2004 Piore Award and to Quebec to receive its 2008 von Neumann medal, Dr. Lamport has not taken the hint and continues to return to his home in California, where he exemplifies his country's low standards by his membership in its National Academy of Engineering and National Academy of Sciences.

We depend on computer systems that are not dependable. No one knows how to solve this problem, and I don't pretend to. But a better understanding of what those systems do just might help a little. The tool that people have been using for centuries to understand such things is math. I will use very simple math to explain what computation is.