I would suspect that a large fraction of them are mathematicians and not particularly interested in how people program.

I wouldn't say I'm intimately familiar with type theory, but I'm certainly old slash grumpy enough to not be an "advocate" of anything except learning both and thinking for yourself about the problem at hand.

CS departments are where people exposed to Type Theory tend to be exposed to it. The sorts of languages that tend to be taken seriously in such departments [yes, I know there are exceptions] tend to be statically typed. Java and C++ just have more gravitas than Ruby and JavaScript and Lisps are for hippies.

I'm familiar with type theorie but i'm not a proponent of either of them. Sometimes its better to use static typing and sometimes its better to use dynamic typing. Howeover most of the times I would prefer static typing.

I think in this subset you're mentioning?

I love type theory, but I think a language like Sage[1] is probably the most interesting way forward.

[1] - http://sage.soe.ucsc.edu/

That's a somewhat unfortunate name to choose for a new language given the existence of this well-established system:

http://www.sagemath.org/

Why the 'but'? There seems to be quite some type theory involved in Sage.

I really like the idea behind Sage but I found it kind of funny that in their test cases all the ".out" files are empty because none of the programs actually do any IO. No hello-world for you :P

How do you feel about dependently typed systems?

Sage has dependent types so he probably likes them.

Ah, I misread the intro blurb.

I think that was the joke :)

I think the joke is rather the small overlap between people who advocate dynamic typing and people who know type theory.

which doesn't mean much. it could be that people who would be interested in learning type theory in the first place would prefer static typing regardless, with a similar argument for the case of dynamic typing

That's not relevant to the original point, which was that the fact that dynamic typing enthusiasts not knowing type theory makes debate on the subject not interesting.

Case in point: just look at https://news.ycombinator.com/item?id=7054960 , where someone who apparently likes dynamic types lists a ton of studies done by other people who like dynamic types where modern dynamically typed languages are tested against the best static types that the early 60's have to offer.

The only part I'd change about that diagram is move the "knows type theory" area way down, so that the majority of static typing enthusiasts are not covered either (but so that the proportion of static typing enthusiasts that are covered is much greater than the proportion of dynamic typing enthusiasts who are covered.)

It's depressing to talk about types when living in a world where both sides of the fence consists mostly of people who think static typing means Java, and where new, "exciting" statically typed languages like Go can have a type system that completely ignores all development that has happened in the past 50 years.

Modern static types are actually good, actually useful, and only ever bother you when not bothering you would mean that your code can crash at excecution time.

not necessarily a response to your comment, but i think you underestimate just how much the static/dynamic preference rests on fundamental psychology.

for example, generally speaking i only use basic data structures (lists or hash tables), so introducing types would be over-engineering (note, i'm familiar with e.g. Haskell's type system). for me the idea of typing implies a programming style complicated enough to require it. it's only at a larger architectural scale that i think typing pays off

that said, C# is still my favorite production language.