Annotated Turing

I've finished "Annotated Turing". It's amazing how one person, in his head, managed to create the entire software industry - with elegant solutions and dirty hacks, bugs and features, hardware solution and programming languages and all the things that had to be reinvented over the next 40 years. And he did it without even trying, as a byproduct of a mathematical proof and philosophical thought.

I can perfectly see how Fortran-Algol-C-C++-Java axis evolved exactly along the lines the Turing predicted. I wish I could get a similar book on Alonzo Church lambda calculus - I suspect that would help me a lot in understanding Lisp. And, to complete the list, I guess Smalltalk would be another by-product of Turing's direction, even though that apple fell far from the tree indeed.

One thing I found troubling is the fact that the proof of impossibility of building the "validating" machine does not refer to any properties of the validating machine itself. Rather, it refers to the inherent impossibility of a machine printing a number that depends on the re-execution of that same machine. A gnawing doubt in my mind keeps wandering: if we use the "validating" machine in a different way, would we get rid of contradiction? I need to re-read that part.