Casual tours around proofs Today Ryan Williams posted an article on the arXiv (previously appeared in SIGACT News) containing a less technical version of his recent ACC lower bound technique.

My question is not about the technique itself (of course worthy of immense praise), but it's about the style of the paper.
In the abstract, he writes: 


  The proof will be described from the perspective of someone trying to
  discover it.


Awesome!
In the Background section he adds:


  This article is a discussion about how to discover the proof – a
  casual tour around it. Not all details will be given, but you will see
  where all the pieces came from, and how they ﬁt together. The path
  will be littered with my own biased intuitions about complexity theory
  – what I think should and shouldn’t be true, and why. Much of this
  intuition may well be wrong; however I can say it has led me in a
  productive direction on at least one occasion.


This is amazing and it's the first time that I have seen it. I have always wondered why authors of paper don't write how they got to the proof, including the failed approaches they tried before getting to the track that led the solution. When I saw Ryan's paper on the arXiv, I felt very motivated to read it. 
I consider it a revolutionary paper from this point of view. Most of the time the only thing you can do with a paper is verifying its correctness.

The question is the following:


are you aware of other papers in TCS where a breakthrough result is presented in a "casual tour" rather than a series of technical lemmas?


I am talking about publications in journals, not blog posts or technical reports.

Also, I tagged it as big-list, with the hope that it will actually be.
Tim Gowers is a fan of this kind of thing.  See specifically his exposition of Razborov's method of approximations.

In his introduction, Gowers references my expository article on forcing, which is a (not entirely successful) attempt to do the same thing for forcing.  Forcing is normally thought of as a technique in logic and set theory, but it has found its way into TCS occasionally.  It comes up in the study of bounded arithmetic and propositional proof complexity (Krajíček and Takeuti are two researchers who have pursued this connection), and the concept of a generic oracle is related to the concept of a generic filter.