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

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