Explicit annotations are not required in many statically typed languages, e.g. with Hindley–Milner type systems, which (like Julia) use type inference.

The difference, as @StefanKarpinski has often put it, is that in a static language it is an error if type inference fails, whereas in a dynamic language like Julia the inference is just an optimization.

Good points, thanks. How about this for the first paragraph:

Types in Julia establish distinctions between different kinds of data, and are used by the compiler to infer the intended use of those data. Programming languages have traditionally employed one of two quite different type systems: static type systems, where expressions must have a computable type before the execution of the program, and dynamic type systems, where types are only computed at run time, when the actual values manipulated by the program are available. Statically typed languages typically offer faster execution of programs, while treating any data of unknown or invalid type as an error. In these languages, the programmer is responsible for ensuring the validity of all types of data that the program may encounter. Dynamically typed languages, on the other hand, do not explicitly check types, and types of data only become invalid when they fail to support run-time operations.

Statically typed languages typically offer faster execution of programs

The whole point of Julia is that this is not true — they are not any faster than type-stable code in Julia. The main argument for static typing, IMO, is safety — by being stricter about types, the compiler can catch more bugs. (And, of course, there are tradeoffs, e.g. in making interactive exploration more difficult.)

But the pros and cons of static vs. dynamic languages is a longstanding debate and a bit of a can of worms here.

I guess by "typically" I probably meant "usually", but I can understand if this unintentionally suggests that Julia is not performant. I'll think about a better wording here.

I don't think "usually" is any better

Statically typed languages offer stricter guidance for avoiding unsafe code, such as treating any data of unknown or invalid type as an error. In these languages, the programmer is responsible for ensuring the validity of all types of data that the program may encounter. Writing programs in statically typed languages is, therefore, more laborious, and interactive exploration of data at run-time becomes more difficult. Dynamically typed languages, on the other hand, do not explicitly check types, and types of data only become invalid when they fail to support run-time operations. This provides a more flexible and productive programming experience, at the cost of a greater potential for programmer errors to cause bugs during execution.

?

of course except for Tuple

I didn't know about that, thanks. Is there a reason why that is the case that we can/should highlight here?

I'm not familiar with all the details but my understanding is that the reason for covariance is largely vestigial; it made dispatch easier in the early days of Julia or something

Tuple type covariance is described here in the docs https://docs.julialang.org/en/v1/manual/types/#Tuple-Types-1

and there is an open issue discussing the potential to switch to invariance in a hypothetical breaking release of Julia (although as a gambling man, I wouldn't put my money on that change ever happening) #24614

I would think a quick link to the docs is probably sufficient