The main advantage of program verifiers (e.g. Dafny) is that there's no (or very little) type/term division. A runtime function `+` is the same as the proof/mathematical function `+`, runtime numbers are mathmatical numbers, etc. (it gets a bit more complicated with equality AFAIK). As a result, in Haskell you have to reimplement the whole (Peano) integer arithmetics again in the type system to prove e.g. array bounds checks, whereas Dafny automatically maps between proofs and code.
I think that Haskell is slowly doing away with this (they're unifing the term and proof language). I think that Idris completely unifies the two. The only difference that remains then is that Dafny uses an automated theorem prover (Z3), whereas in Haskell/Idris you have to do proofs by yourself.
In short: no. It's exactly as cumbersome. If you look at the other comments you'll see plenty of people that found it hard to work with. Equally, if you look at Idris mailing lists you'll find people who love it.
Another way of looking at it is which is easier to grok: imperative or functional flow.
It's complicated. Basically, verifying programs is hard and pretty cumbersome regardless of the formalism, and the differences in the theory don't matter too much for most things people do. Having said that, making practical use of dependent types is currently behind proof tools for direct logic (in terms of automated provers, model checking etc.). What people sometimes do is start with direct logic expressed as a contract (say, like in Dafny, Java with JML or Ada SPARK), run automated tools on those (SMT solvers), and if the solvers fail, generate obligations for a logic based interactive prover or a dependent type one, at which point the differences matter even less. But working completely within a dependently typed language is currently unrecommended unless you just want to learn or play a bit, or unless you're an expert. Dependent types are just not yet "production ready".
