A crash course in the mathematics behind Turing's results and how it applies to the very practical problem of programming in C. Explains the connection between Turing Machines, Lambda Calculus, types, Classical Logic and proofs.