Lambda the Ultimate

First, assume Statically typed languages are superior

This paper doesn't assume statically typed languages are "superior" in any serious sense. Except, perhaps, at catching type-related bugs automatically at compile-time.

... And that a correct type system ensures "code in typed modules can’t go wrong"?

This phrase is a refinement of a popular slogan commonly used for proofs of soundness for static type system that claims that "well-typed programs can't go wrong." The notion of "going wrong" is a pithy (if misleading) way of saying "cause runtime type errors." This is what static type systems are supposed to prove can't happen.

However, even in statically typed languages like ML or Haskell, there is always some interaction with the underlying system (via the standard library or FFI) that relies on something outside the system respecting its types. So, in face, the notion that "code in typed modules can't go wrong" is a more accurate reflection of the guarantee that you get from a statically typed language: you might get a runtime type error, but it won't be caused by well-typed code.

So what would be the best use of your time: writing more unit tests or converting your dynamic program to a statically typed language?

You sound like you're disagreeing with the paper, but you aren't; the paper is specifically describing systems in which you don't have to migrate an entire program from one language to another, but rather the language supports both dynamic and static typing and allows you to migrate code piecemeal.

are doomed to reinvent them test by test.
You might be able to write tests that reproduce the functionality of Diakon, ESC/Java, Houdini, and others but it would take more time than calling them (to say nothing of Spark Ada). A C2 page that discusses writing unit tests for concurrency.

While there are some approaches for testing concurrent programs, I believe testing distributed software is even more complicated (I am being puzzled by this problem, anyway).
OTOH, type systems also are not really helpful in distributed setting (yet).

...that I now am compelled to refer to Acute and HashCaml again, just to remind some folks that "yet" isn't necesssarily quite as far off as it may seem at first blush. Thanks for the setup! ;-)

And Alice ML also has type-safe pickling and distribution since its very first release, if I may add. But I fear that Andris alluded to something stronger than mere unmarshal-time type checking as found in these languages.

I'd rather see this amount of effort go into, say, static type analysis systems for popular scripting languages instead.

'Cause lemme tell ya, when I have a big project written in a scripting language working well, of course I'll want to reinven^H^H^H^H^H^H^Hrecode a bunch of it in another language and deal with language integration headaches.

...an "amen" here.

The closer we get to a genuine "slider" for "static" vs. "dynamic" typing (dependent types? abstract interpretation?), the better off we'll all be.

I'd rather see this amount of effort go into, say, static type analysis systems for popular scripting languages instead.

That's not the way how things work in the OSS communities these days. Guido decides to throw annotation syntax to function arguments and return values, leaving unspecified what these annotations shall actually mean. Now dozends of willing programmers are going to implement annotation handlers including type checkers with different kinds of policies and semantics. The best fits might be chosen any time in future to become part of the standard library. Even better than breeding articles/programs is breeding programmers. Not sure if anyone of the implementers reads scientific papers or is particularly interested in Scheme? Sociology matters as always.

BTW it is a common practice to factor certain perfomance critical parts of a script into a "real" programming language i.e. language which is just too painfull for writing scripts. So annotating types might be the cheapest way to cooperate with the compiler to do all the optimizations and produce native code - if this is required...