Whenever I do leetcode, I use python. This is because most of the constraints that are useful to check in an algorithm can't be encoded as types. Instead I sprinkle a lot of asserts (possibly using slower bruteforce version of the code) to check invariants and properties that I expect to be true.

I think dependent types is supposed to solve this problem (for example, rather than just a list of ints, it can encode that it's currently a sorted list of ints) but they don't seem practical to use at the moment.

In some sense, yes.

But it's a test suite that can be much cheaper to write and maintain.

> Or the converse “your type system is basically a very limited test suite.”

the converse doesn't hold. You can write new code that will benefit from the guarantees of existing types. But you'd have to write new tests if you didn't have types.

Not necessarily. If you add new code to the user signup (let's say some additional checks on the shape of their username) and the integration test for the happy path of a user signup still passes, the new code is absolutely covered by existing tests (though probably not completely, there are probably edge cases not covered).

The tests/types correspondence still holds: if you write new code, you will often also need to alter the types to correctly describe the changed domain. In the username example above, after adding username validation it would be a good idea to have a dedicated `Username` type that can only contain valid usernames instead of just stuffing everything into `String`. If you count extra time writing and refactoring tests after adding new code, you should also count the extra time writing and refactoring additional types after adding new code.

I think that’s where our experience with type systems could be used to improve our testing methodology and technology. Having the ability to reuse tests in client modules would effectively fix that gap (eg by generating fakes for the original modules from its tests).