A number of wonderful (literally) thoughts are wrapped up in Ian's item on testing, Dijkstra, Turing, and beautiful code.
One at a time...
On point 1, I would say that developing in a test-driven way is kind of like developing proofs incrementally. Once your code passes the tests, you have not proven the absence of all bugs, but you have at least proven the absence of all bugs you thought were important at the time. So you are not done, but you are significantly closer to being done.
On point 2, I would say that rereading (and refactoring) to achieve "conceptual integrity" is kind of like making a proof more comprehensible. You have done the messy work, now make sure it is presentable so others can use it, extend it, or carry the "proof-in-progress" further with more tests.
On point 3, I would point out that the lambda calculus is not talked about enough in computer science education generally. Developed by Alonzo Church, a peer of Turing, the calculus is both equivalent to the Turing Machine and closer to modern programming languages than is the Turing Machine. (Of course, it doesn't have I/O either, so I am not sure what to do about that argument.) Programming language semanticists as well as compiler writers actually use properties of the lambda calculus all the time. I am not sure the same could be said for the Turing Machine.