[groos]

A couple of decades ago, I attended a lecture by Tony Hoare about program correctness. He used the producer-consumer problem as an example and by starting with pre/post conditions and refining them, he arrived at a (proved) correct program. I went back from the lecture thinking this is so easy, I can apply this as well. Sadly, I realized one has to be Tony Hoare to produce code out of logic with his level of ease.

[rikthevik]

Sometimes I read a paper or see some code that makes me think that wizards are real and that they walk among us.

[schoen]

Apparently some aspects of Idris, Dafny, and (maybe) Isabelle are helping less-awesome logicians derive programs from their specifications nowadays.

(I haven't tried any of these languages so I don't have a personal story of how helpful they were for me.)