Butler
Lampson
Microsoft
Turing Award lecture, 1993
We have learned depressingly little in the last ten years about how to build computer systems. But we have learned something about how to do the job more precisely, by writing more precise specifications, and by showing more precisely that an implementation meets its specification. Methods for doing this are of both intellectual and practical interest. I will explain the most useful such method and illustrate it with two examples:
Connection establishment: Sending a reliable message over an unreliable network.
Transactions: Making a large atomic action out of a sequence of small ones.