A very interesting article by the creator of quicksort on his contribution of axiomantic semantics to programming languages (the infamous Hoare triple {P}Q{S} [
1]). What strikes me as most interesting is his idea in chosing software verification in the first place (albeit funny!), and the surprises he had in hindsight. (Which almost always makes for an interesting read, cf. Niklaus Wirth: "Good ideas through the looking glass".)
[1]: Interested readers might want to check out the excellent "The Science of Programming" by David Gries.