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.

Although he talks a bit about formal specifications and tools for writing and verifying them, his talk has a few really great parts about informal specs.

I'd recommend watching 23:22-30:42, where he gives an example of where an exhaustive semi-formal spec was critical for writing good code.

I'd also recommend 44:00-54:00, which I think is the most broadly applicable part of the talk, where he discusses the need for thinking as writing, and writing specs before coding.