Leslie Lamport on Specifications Before Code

HN points people to it as Lamport's own case for thinking and writing a spec before coding, and as an entry point to TLA+.

Leslie Lamport argues that programmers, like architects, should write rigorous specifications before coding, especially for concurrent and distributed systems. The talk introduces the case for writing specs (the TLA+ mindset) as a way of thinking above the code.