[tmoertel]

+1 to this book. Developing algorithms and their correctness proofs together is a powerful technique and ought to be more widely used.