I don't understand what you mean by encoding tax. Can you give an example? Certainly lots and lots of work to make an actual practical and usable system still needs to happen, but I don't see any fundamental limitations with respect to effects, including non-termination.

> For a start you have to prove termination, even when you use simple types.

This is not the case. E.g. in Idris you have non-terminating functions. In NuPRL the whole thing is built on potentially non-terminating functions. Of course the functions that you use as proof witnesses have to terminate, but that's true in any system since a non-terminating proof witness means that the proof is bogus ("Theorem: Socrates is a goat. Proof: Socrates is a goat because Socrates is a goat."). The functions in the program that that the specification is saying something about do not have to be proven to terminate.

> (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

I don't want to prove that I didn't need the cast or check, I want to not have the cast or check in the program in the first place. This is about types that are expressive enough to model the actual shape of the data, not about proving that a program is correct relative to some specification. By analogy with lacking generics / parametric polymorphism like old versions of Java: if I write a program that uses a List I need to cast to and from Object. With generics I can use a List<T> and do not need the cast. I don't want to write the program with casts and then prove that I didn't need them, I want to write the program with List<T> without casts. For the same reason that you still want generics even if you use a program logic to reason about your programs, you still want dependent types even if you use a program logic to reason about your programs.

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

Why? You can write the same program without specification as you would in the program logic system, and then prove lemmas about it.

> the beauty stands in the way of type inference

Type inference is overrated anyway, and with dependent types you don't actually lose type inference. You do lose it for the parts of the programs that use fancy types, but you wouldn't be able to write those at all in a language with full type inference. There is no fundamental reason that a dependently typed language couldn't have the same type inference for non-dependently typed pieces of the program as the language that only supports non-dependent types.

By the way, and I admit this is more of a theoretical curiosity, IIRC full type inference for dependent types is decidable if you do not have implicit parameters. That does make sense: you can either infer types, or values, but not both at the same time. Of course in practice you much rather have implicit parameters than type inference. From the proof assistant side of Curry-Howard type inference is also kind of strange: you infer the theorem (the type) from the proof (the program). So it's like writing down a proof, but having it inferred what the proof is actually proving.

> the Hindley-Milner polymorphic typing system "has hit a sweetspot"

Where sweetspot = local optimum :) Meanwhile, OCaml is getting GADTs ;-)