Thanks your your reply.

Idris has ... is that not satisfactory?

I'm not an expert in Idris, but I think effects are encapsulated /
encoded somehow in Idris. I don't think full Idris a logic, only the
pure sublanguage (please correct me if I'm wrong), so you loose the coincident between programs and proofs. That probably means
that there is some "encoding tax" when reasoning about stateful
computation. The more complicated the effects the higher the encoding
tax. Just imagine you'd have to reduce full concurrency
(e.g. pi-calculus) to lambda-calculus. That would be painful.

It is perfectly possible to program in them like you would in a normal language.

I don't think that's true with current systems. For a start you have
to prove termination, even when you use simple types. (Which leads to
another shortcoming of the Curry-Howard approach to verification,
non-termination.)

I regularly run into situations where I think "gosh, if I had dependent types

Sure, and I often think the same. But that doesn't address the key
point: (1) you can always do the same with program logic, prove that
you don't need a cast, but more imporantly (2) in a lot of large-scale
programming projects, you don't have good specifications
up-front. Instead you have a vague idea, and try to knock out a
prototype as soon as possible to show to the customer, who will
typically then reply "that's not quite what I want instead ..." and
you go back to the drawing board and iterate. The specifications and
the program coevolve. In prototype stages you don't actually care if
the program needs a cast or not, you just put in the simplest thing
that works, and fix/optimise later, probably only after heavy
profiling. Who cares if a missing-cast exception is thrown during the
protoptye phase? And for large projects the prototyping phase might
already involve a team of 50 programmers. Since good specifications
are typically only available at the end of a project, when the
software is stable, it only really makes sense to pay the (currenly
enormous) cost of full verification at the end of the project. With program logic you can easily
delay verification until the end of the project (but don't have to),
with Curry-Howard based verification you can't.

Two, type system researchers promote provably correct programming as the advantage of dependent types.

Program logic researchers promote provably correct programming as the advantage of program logic. Anyway,
programs can only be provably correct w.r.t. to a specification, but
in most programming projects, a meaningful specification is not
available in the early stages, so any talk about provable correctness is inapplicable.

they generalize a vast swath of different type system features

I fully agree with you here, and it's beautiful. But the beauty stands
in the way of type inference, and that makes full dependent types
extremely costly for most (but not all) forms of software
engineering. As B. Pierce says: the Hindley-Milner polymorphic typing
system "has hit a sweetspot" (B. Pierce) between expressivity,
type-inference and simplicity.

Furthermore, if you want it's possible to use a program logic style of verification in a dependent type system.

I'm not totally sure I can' follow you here. How does this get around the totality issue?