At the beginning, Leslie explains why specification is important. He gave few convincing (me) examples and then introduced the idea of formal specifications. T

At the beginning, Leslie explains why specification is important. He gave few convincing (me) examples and then introduced the idea of formal specifications. The formal specification allows you to find design bugs, before writing any code. An anecdote about XBox memory model is given: a certain hardware bug (in the memory unit) once made it's way into production would stop any XBox after 4 hours of using it. The bug wouldn't be found using any methods the hardware manufacturer was using. The bug was found due to an engineer who was formally specifying the memory model. He provided a bug description and the response was: "Invalid, the system cannot come into this state". The engineer than responded with a scenario leading to the state using the rules which governed the memory model. Eventually the bug was fixed. Leslie moved to more down to earth examples: finding greatest common divisor (Euclid's algorithm) and QuickSort. They were expressed in pseudocode and with minor adjustments as a TLA spec. In all examples the same conclusion was given: having written only the code it would be very difficult to find the design bugs.