Earlier quoted context omitted.
Unfortunately, I don't think type theory has a whole lot to do with programming or software engineering. The most practical languages (as measured by popularity, which seems to be the best way to do it over a period of decades) do not have sound type systems, nor even particularly interesting ones theoretically.
You should reconsider your stance. Types allow requirements changes to be propagated through all program. State-of-the-art type systems even allow accounting of effects, like prevent deadlocks by ensuring a specific order of locking: http://www.cs.st-andrews.ac.uk/~eb/writings/fi-cbc.pdf This is just another tool in a toolbox. You can use it. Or you can throw it away as "no one seem to use it".
"Types allow requirements changes to be propagated through all program" - what does this even mean, and why is it a justification for powerful types? I designed a system once that let you describe the program at a high level, using a DSL. I've outlined it several times on this site here (here's one link: http://news.ycombinator.com/item?id=2192322). Now that system allowed requirements changes to be propagated throughout the whole program, because the level of description of the program was dense enough that it could just about be considered detailed requirements (i.e. it was powerful - see below). It worked because it was focused on a reasonably precise niche. It did enough checks during the compilation process that you could be fairly sure that if it didn't find any errors, it would work without bugs (i.e. it was good - again, below). But the level of type system it had was no more advanced than Pascal - and I mean early Pascal, no objects etc. If you can get the same effects without a very abstract and powerful type system, isn't that better, because it reduces the overall expressiveness of the language - i.e. reducing the solution space that needs to be searched? Form can be liberating.
Preventing deadlocks by ensuring a specific order of locking. Fantastic; good work. How many people are using it? Which large shipping systems are using it? What was the prior rate of deadlocks for similar systems at that level of complexity, how long did those deadlocks take to be fixed, and how much time and money was saved by using this new technique? Because frankly, deadlocks are trivial to debug; the relevant threads are stopped, and after you attach a debugger the stack traces tell you exactly which locks were taken and in which order. Debugging races is a wee bit harder.
I have TAPL by Pierce right here on my bookshelf. Here's a typical sentence which illustrates my problem: "Perhaps the best illustration of the power of recursive types is the fact that we can embed the whole untyped lambda-calculus - in a well-typed way - into a statically typed language with recursive types." (pp 273). It seems to me to take for granted that a statically typed language is good[1], and that a good measure of power for a statically typed language is how expressive it is (i.e. what shapes of programs it can express, not e.g. how syntactically light it can be in doing so). And this is probably right and good, for type systems. But I have a different perspective of "good" and "power" in a programming language (as distinct from a type system). A good language is one whose target audience finds it easy to express their intent in such a way that the computer can understand. A powerful language is one in which complicated effects can be expressed with succinctness. And this is the core of it: type theorists spend entirely too much time on theoretical benefits, and far too little time on whether these benefits are worthwhile. Perhaps that's not their job, you say: and I agree to you to the extent that you also agree, then, that much of their work is irrelevant because of that.
[1] I happen to like statically typed programming languages, but I understand why some people don't. I wrote an extended reply on this topic to Paul Biggar some time ago, again on this site: http://news.ycombinator.com/item?id=1110653