[1] of the countably infinite possible programs, virtually all
If instead I have a good idea what I want to write, the type system may either guide me towards the solution, or hinder me. It usually hinders me, I don't need a type system to guide me, but I like a type system that can check for trivial errors (oh, I meant to pass a list of numbers, not just a single number).
Not to mention the tools to debug complex type errors are generally much less mature than the tools to debug runtime errors.
But even so, I think we could still benefit from going a little further towards the "proof" end of the type system spectrum in most cases. I don't think anyone really wants to deal with Coq and similar, but having used a language with dependent types for integers and vector lengths it's really nice to be able to say stuff like "this integer is in the range [0, 8)" and then have it catch errors when you pass it to a function that expects [0, 3) or whatever.
While I generally share your skepticism, I think this is quite wrong. A good part of the point of advanced type systems is to make more complex problems possible while still being well typed. For example, in C, if you want a function whose return type is tied to an input argument's type, you either use void* and casts (no type safety), or you don't write that function. In languages with even slightly more advanced type systems, you can write that function and still get full type safety.
Even more advanced type systems achieve the same things: you can take programs that can only be written in a simpler type system and make them safe. In standard Haskell, for example, you can't write a Monad and actually have the compiler check that it respects the Monad laws - the implementation of Monad functions just assumes that any type that implements the right shape of functions will work as a monad. With dependent types, you can actually enforce that functions designed to work with monads only apply to types that actually respect the monad laws.
The trade-off with very complex type systems is different, in my opinion: after some point, you start duplicating your program's logic, once in the implentation code, but again in the type signatures. For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs.