[mikedodds]

I love Dafny - we've worked on it in the past in fact. Theorem proving is definitely something that's being applied in industry - our crypto verification project uses Coq in some places. There's definitely a lot of hype though, some of which seems a bit unrealistic to me. There's a long, long way to go before theorem proving is practical as a tool for general programming, rather than in ultra-important niches like core crypto libraries.