Earlier quoted context omitted.
"Statically-typed" and "type-safe" don't mean the same thing. "Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-chec…
Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?
However, my main point was that "type-safe" and "type-unsafe" are not synonimous with "static" and "dynamic". The original question was probably about static vs dynamic, but I think it's important to point out the distinction; especially when reading material like Bob's that assumes some familiarity with the terms.
From a Curry-Howard point of view:
* Static types are logical formulas, values are their proofs.
* "Dynamic types" are the clauses of one big disjunctive formula: Int OR Bool OR Error OR Array OR String OR ....
* Safe type systems are sound logics; they don't let us prove "FALSE".
* Unsafe type systems are unsound logics; they let us prove "FALSE", and hence anything (ex falso quodlibet).
Importantly, the big disjunctive formula used by dynamic languages is trivial to prove. For example, I can prove it with a constant like "10", without having to perform any computation. Trivial formulas are equivalent to "TRUE" (the logical proposition, not the boolean value!), hence dynamic languages only allow us to prove "TRUE". This makes them type-safe, since they can't prove "FALSE", but it makes them uninformative: proving "TRUE" doesn't tell us anything we didn't already know!
The only languages which can be type-unsafe are static languages, since they're the only ones which can express types other than "TRUE" (eg. "FALSE"). If a static language is unsafe, then there's essentially no benefit to it having static types, since we can't trust any of the information it gives us.
That's why academics prefer type-safe languages, whether they're static or dynamic, whether or not you agree with Harper that one's a sub-set of the other. Unsafe languages specifically hinder our reasoning. Sure, we might be confident that our particular C program is safe, despite C being an unsafe language, but we can't generalise that to "for all C programs 'P'...", which makes it difficult to study languages-in-the-abstract. Of course, we lose nothing if we make the language safe, so we might as well do that (eg. define a safe sub-set of C like http://compcert.inria.fr/doc/ ).
Essentially, asking "Why do programming languages researchers seem so enamored with type-safe languages?" is like asking "Why do Mathematicians seem so enamored with sound logics?". Of course, there is research in non-monotonic logics, para-consistent logics, etc. and that's great, but if we're going to have an academia-vs-industry debate, then I think the unsound logics, and hence the type-unsafe languages, have the taller ivory towers.
Of course, there are many other ways that static and dynamic languages may be safe or unsafe (eg. memory safety, thread safety, non-total, etc.). (Safe) type systems can eliminate some of these problems (eg. memory safety with linear types), but just because it's possible with some type-system feature doesn't make a language lacking that feature type-unsafe; the worst we could say is that it's type-uninformative.
For example, Haskell's type system doesn't distinguish total functions (eg. via a data/codata separation). This makes Haskell unsafe with regards to termination/cotermination, but it doesn't make Haskell type-unsafe. Since dynamic types are completely uninformative, they can't solve any problems that type systems are suited to, but that still doesn't make them type-unsafe.
For example, it's not that dynamic languages allow type-unsafe operations like passing strings to "+ : Int -> Int -> Int", it's that dynamic languages don't allow us to restrict the type of "+" at all; we can't even specify that it's a function, let alone what that function's input and return types are! If it generates a run-time error that's fine, since "run-time error" is a perfectly valid value, as far as the type system's concerned.
Now, we may think this is an unsafe thing to do, but it doesn't make the language type-unsafe. It just makes it "semantically unsafe" or "unsafe without lots of tests" or somesuch.