Why this lecture is important

Proofs are the essence of mathematics, and mathematics is--believe it or not--the soul of computer science. The most interesting and elegant programs and algorithms have to be grounded in theory. It is our ability to prove properties about algorithms that makes them useful. Lamport's talk addresses the problem of constructing a proof, something that's harder than most of us realize.