In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s.  See this short note for Turing's original proof and some historical comments.