A good type system will help with # 2, 3, 4, and 6 too.

In fact, types are better for #6 than tests, because they have lower overhead, so they are more likely to be complete at the interruption.

Agreed on the first 3.

I think you might have misunderstood #6, because I don't see how a type system can function as a todo list.

As I am writing my code, I try to make sure that when I need to make a change, I can make part of the change and the type checker will surface everything that needs to change in tandem (not always in a single run). The todo list is then simply the list of remaining errors, and I can usually jump right to exactly where the fix is needed.

This sometimes works out really impressively well. There was a time I was working on a project that required really low latency at low-to-moderate throughput. It was greenfield C development, fairly experimental. I made a habit of tagging functions with an argument describing which of the statically defined threads the function needed to live on, tagging data with which thread it should be accessed from, and checking agreement between them (without runtime overhead).

This couldn't be rigorously enforced by the type system - C has way too many escape hatches - but it was easy to build a little bit of infrastructure such that doing it right was significantly easier than doing it wrong, and doing it wrong was obvious.

When (as is inevitable) we discovered that we wanted to do significantly more work somewhere and so wanted to move it out of the hot path, or discovered that some new thing we wanted to do unavoidably had to now live in the hot path, &c, I could move code between functions and the compiler would tell me everywhere I was doing something that didn't belong in the new thread.

Huh.

hmmm....

You know, I think you've just revealed something about the shallowness of my experience with type systems.

Defining a test like:

    # Checks if the user has the correct authorization
    log(non_authorized_user)
    def some_action:
        assert_failure(user_has_authroization)

isn't much different from checking that on the types:

    data AuthorizedUser authorizationSchema = AuthrorizedUser User
    someAction :: AuthroizedUser ActionAuthorization -> IO ()
    someAction = undefined

Yes, compile-time type-checking can be replaced with a sufficient quantity of runtime type-checking in the form of unit tests.

However, the compiler's type-checking is automatic, so you don't have to write a ton of unit tests to get its benefit, and the error messages are usually much better.

I've yet to see a dynamically typed codebase that has sufficient unit tests to replace a decent compile-time type-system.

One other point that matters is time: running 20k unit and integration tests to verify the types are all correct for your 6kloc will take much longer than compiling 6kloc, and the compiler does a much better job of updating incrementally based on code changes than any unit testing framework I've used.

> One other point that matters is time: running 20k unit and integration tests to verify the types are all correct for your 6kloc will take much longer than compiling 6kloc

I'll disagree here. The kind of thing you can verify at compile-time can be tested very quickly, and compilers with less useful type systems can be much faster. All in, the tests are probably faster to run.

But yeah, compilers do make a better job on incremental validation. That's probably intrinsic; validation is very likely more prone to be incremental than tests.

> The kind of thing you can verify at compile-time can be tested very quickly

I’m not sure I entirely agree with this. For example, a type system can ensure a function is always called with the right units, but testing that every use of the function is correct might be a lot more tedious, depending on the code base.

> and compilers with less useful type systems can be much faster.

This depends very heavily on the language (e.g., OCaml being a language with a relatively complex type system that also compiled fairly quickly), but Id agree that what you said appears to be the general trend.

for instance, https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type...