Casual tours around proofs
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.