In 1936 Alan Turing wrote a paper "On Computable Numbers, with an Application to the Entscheidungsproblem [0]". The most interesting result of this paper is not the conclusion, that there cannot be a general solution to the Entscheidungsproblem, but how Alan Turing reached that conclusion. In his paper he introduces a computing machine (a Turing machine) with a limited number of operations, by showing that such a machine can not determine the ultimate fate of all other machines, he proves there is not general solution.

In 2008 Charles Petzold wrote "The Annotated Turing", in this book he dissects the original paper from Alan Turing. This book not only presents the original paper (and the appendix and corrections) with numerous annotations and samples, but also is a biography of Alan Turing's life and an introduction to the mathematical background, required for understanding the paper. The book concludes with an overview how the Turing machines can be used to help understand the human mind and the universe.

This is a highly recommended book, which is very accessible for anyone with a general interest in computes and mathematics. And a must read for all developers, who want to understand why there can't be a general program which verifies all programs are error free.

[0] The Entscheidungsproblem asks for a general decision procedure with a finite number of steps to determine the provability of any given well-formed formula.