This might be the best article that I have read this year. It might change the way that I program. I really want to write up examples for each of the ideas presented: Monotonicity, Pre- and post-conditions, Invariants, Isolation, Induction, and Proof-affinity as a quality metric. I think it's easy to find these ideas in my code, but I want to try to practice writing proofs "in my head" as I code to make my code better. It is not apparent to me now how this will work, but if I write up some examples, I imagine it will become clearer.