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