I never said "no one seems to use it". What I specifically said was that I don't think type theory has a lot to do with programming: i.e., that the majority of work put into type theory in academic contexts does not, on balance, do much to improve the state of programmers writing software, or the quality of our software engineering.
"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
You are right that many people don't need the results of type theory for their work. But that mainly tells on the type of work you do. For example many people think programming does not need math but if you are writing physics engines, graphics engines or doing machine learning then you need some basic level of mathematical sophistication. Similarly, if your work is related to automatic verification or the transformation from code to code then knowing type theory will save you a lot of wasted effort reinventing pitfalls. Type theory gives a foundation and a why basis so that intuition can be augmented beyond rules of thumbs. Language Oriented programming is one which would benefit from such a knowledge. Consider also that the future is not going to be dominated by one platform, powerful code transformation tools will be a strategic advantage. Know that my emphasis is not on the strength of the type system just its consistency and ability to augment human reasoning.
Software engineering is the only field of engineering whose practitioners do not use a basics grounded in math. Electrical people have Maxwell, ohm, gauss etc. Mechanical engineers and dynamics, civil continuums and so on. None of these professions you will note, came after the math. The math came as a result from studying and generalizing on these and then feeding the results back providing a net gain for both. This leads me to believe we are in early stages yet. We have the catapult without trigonometry. We do not have enough understanding to build stuff to withstand earthquakes. You say that most languages don't have well founded types but you fail to note that many of those same projects often have massive teams, massive code bases, fail often, run over time and are insecure.
But all that said, programming is different isn't it? You can get instant feedback and build something that you think is good because it fits all the white swans you put inside it. So I think before we have a foundation we will need tools that are built from and require a basic understanding of category theory and types. These can then be used to quickly iterate tests and do so with strong guarantees without having to write annoyingly tedious constructive proofs. Genetic programming is stupid but what if it could reason about types and try hypothesis on a meta level as well? Or what if tools such as http://lambda-the-ultimate.org/node/1178 were developed into the typical programmers toolchain? But yes, complex types without tools are a hard sell.
Code transformation has historically focused on syntax, but fallen down on semantics. The devil is in the fine details; C# might look superficially similar to Java, that you might create a code transformation from one to the other, but you end up falling down in really thorny areas like order of class initializers and finalization semantics, not to mention of course differences in scope and substance of libraries, standard and otherwise. When your code is pure and functional, you can make much stronger statements about it. But I think it's still an open question as to whether functional code can be made practical in the large.
"You say that most languages don't have well founded types but you fail to note that many of those same projects often have massive teams, massive code bases, fail often, run over time and are insecure" - are you suggesting that correlation is causation? Of course you aren't. But you might be guilty of thinking that something must be done, powerful type systems are something that seem good, therefore they should be used. And it's precisely this kind of implication that I'm skeptical of. When we start seeing substantial bodies of industrial software using advanced type systems rather than incorporating more limited, less orthogonal and less general subsets, I'll dial back my skepticism; but I'm willing to bet, at this point, that if that does happen, we won't have seen the end of massive software failures. I think that's a social problem, not a technical one. Our reach forever exceeds our grasp.
As I mentioned in my earlier post I do not think it is the power of the type system that is key but its consistency and the accompanying tools. I am not saying programming in Coq or dependent types are the answer. I am asking, what if programmers had access to a more polished toolkit to create domain specific versions of djinn where it would guide them or help layout some basics? Knowing that the code was derived from sound axioms. Other engineers can quickly protoype the validity of their ideas by mechanically running through some equations, why not software engineers?
Already I use types in Haskell and F# to help me figure out how to layout the code - I write some basic code where I know which function it will feed into, I don't have to think much as I try to get the code to fit the types. Nothing fancy but still highly useful.
As for code transformation I don't mean generic stuff like Visual Basic to Java, I mean having a team able to write the tools themselves with full awareness of the requisite semantic mappings. Or even better, creating a dsl for the domain and then having that map down to appropriate platform specific code. But it need not be traditional development you could extend it to machine learning - say you are doing genetic programming to fit data, using types to have some level of axiomatic reasoning rather than random cross over may be fruitful. There are all sorts of uses where application of basic - not fancy theory is helpful.
"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