The book 'The science of programming' of David Gries is also a nice introduction to writing programs using mathematical logic and reasoning. The book is inspired by the techniques of Dijkstra and Hoare, and written in a way that's easy to follow.
I looked that up and got this sample of that book: http://www.cs.cornell.edu/courses/CS5860/2011fa/documents/Gr...
Looking up Stepanov's book, landed on his slide deck about the book.
Interestingly enough, both are about the remainder algorithm, and Gries' mentions a "large program" of "3000 lines", which reminded me of the other comment and the 3000000 to 30000 figure.
[Stepanov's deck: http://stepanovpapers.com/EoP-StanfordEE380.pdf]
http://blg89.net/blog/wp-content/uploads/2013/11/The-Science...