That sounds about right. Static types can only guarantee a certain subset of behavior. Unit tests work for a huge amount of behavior, because they run at run-time. They are very versatile. But there are still some things that unit tests cannot test.
In particular, unit tests cannot guarantee the absence of behavior. As an example, Haskell can use its static type system to say, "this function (and any functions it uses) is guaranteed to be pure". Or you can say, "this function (and any functions it uses) is guaranteed to only use certain side effects, but other side effects do not happen".
Languages like Idris go even further and can guarantee that a function terminates (never goes into an infinite loop)!
As another example, Haskell has Software Transactional Memory, and it uses the static type system to guarantee that arbitrary I/O cannot occur, which is important because the transaction might be retried multiple times.
I don't remember which language it was in, but I remember reading about a language that used static types to guarantee that exceptions are always handled. In other words, you will never have an uncaught exception.
As you are aware, Rust uses its static type system to guarantee that pointers are always used correctly, and that data races cannot occur, even with concurrency.
But the biggest reason I like static types is because they make refactoring easier. Let's say you have a type that represents a person. So you have a name property, age property, etc.
Now let's say you want to add in a new property. Some of the existing functions will need to change to accommodate this new property. Without static types, you need to carefully go through your entire code base and find the functions which use the type, and then change their behavior to work with the new property.
Unit tests won't help you with that, because the unit tests are all testing the old properties, not the new property. So in the end, you have no choice but to just bite the bullet and spend a significant amount of time searching through the code and making the changes.
But with static types, it's as simple as adding the new property, compiling, fixing any type errors, compiling, fixing any type errors, etc.
Each type error tells you the file and line where the error occurs, making it easy to fix. You don't need to search through your code to find the places which need fixing: the type system does that for you. And after all the type errors are fixed, it's basically guaranteed that your code is correct.
Another example: a function used to always return a result, but now you need to change it so that it can potentially fail. So anybody that uses that function now has to account for the possibility of failure. With a static type system, you simply make the change and fix the type errors.
With unit tests, you better hope that you have 100% code coverage, because you're going to need it to find all of the functions which need to be changed. And don't forget that the unit tests need to be updated, and you probably need to add in new tests as well. That takes time, in addition to the time spent fixing the code.
So the end result is that it's faster and easier to refactor with a static type system, and it's more likely to be correct as well.
So I think static types and unit tests complement each other: they can both do things that the other cannot. Static types can make guarantees that unit tests cannot, and static types also remove some of the burden from unit tests, which speeds up development without sacrificing correctness.
On the other hand, unit tests can make certain guarantees that static types cannot. So in the end, I think you need both.
P.S. Static typing also helps tremendously with things like smart IDEs. I think Unison is a really cool example of that:
Typeclasses are amazing. They're similar to multimethods, but more powerful, and they have the same performance as regular functions.
You can use them to solve the expression problem, giving you a huge amount of flexibility, power, and conciseness. Or you can use them to create dynamically scoped variables which actually work correctly (unlike dynamic variables in most languages).
The thing is, typeclasses are only possible with static types. They're the main reason I changed Nulan to be statically typed.
By the way, I would like to point out that the static type systems in languages like Haskell is very different from the static type systems in other languages like C, C++, or Java. So even if you like/dislike one of them, you might end up liking the other. I used to lump all of the static type systems together, but I think that's a mistake.
There are bugs which are not caught by C, C++, or Java, but which are caught by Haskell. And there are programs which do not type check in C, C++, or Java, but which do type check in Haskell.
Yes, I wanted to say something similar in response to your phrasing that "type systems (including dynamic and static type systems) are another way to carve out the territory". When you say "dynamic type systems", in particular, I think Python and Ruby, and the modularity guarantees there seem much inferior to tests. But Haskell and the more advanced type systems might well disprove my thesis.
Yes, that's exactly the trade-off I've been thinking of. When I program I like to start out writing tests at the start when I don't yet know what properties I should try to enforce. Over time I start finding places where tests aren't good enough, and start feeling the need for more rigorous checking. But by then I've painted myself into a corner with my choice of language, and it's too hard to switch to a more rigorous platform.
In Mu my plan to break this dichotomy between coverage and soundness is to allow arbitrary metadata to be attached to instruction operands. As a result you aren't stuck with the type annotations and checking that I build into the system. You can have arbitrary metadata and will be able to write programs that can deduce and check this metadata to enforce all sorts of properties. Arbitrary checkers feels to me like a generalization of Lisp macros.