Butler Lampson
Microsoft
November 12, 2002
Most people use formal methods to analyze algorithms or components (such as a floating-point unit or a string library) and to prove things about them. This is valuable, but I have found formal methods much more useful as tools for understanding the hard parts of a computer system. The idea is to abstract away the easy parts of a system (for example, the details of data structures) in order to get something that still exposes the hard problems, but is small enough to study thoroughly. Then you apply the standard techniques of state machine specification, abstraction functions, and simulation proofs. I illustrate this approach with a number of examples: file systems, transactions, replicated state machines and group communication, security, and caching.
Word, Acrobat. Information about
my MIT course on this subject is here.