[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.)