Typing in modern days is effectively moving the task of debugging to compile/ide annotations process instead of testing for correctness.
Albeit it makes the process easier compared to a really shittly written code without strict typing, but against good codebases, it takes the same amount of time.
If you think about correctness of a program, (i.e for any combination of given input , it changes a state in a determinstic way, including no state change for invalid input).
Strict typing is one way to accomplish this. The cpu does not give a shit about types. It cares about memory registers and locations. The unique code built into the compliers/transpilers is the thing that validates the correctness of the program in this case.
You can move that code into the testing suite without relying on the complier, and just do testing. Generally, given competent programming skills, this takes about the same amount of time as designing a well structured program - your tests are pretty much your design document for the thing itself.
This is a very anti-pragmatic way of looking at things in my opinion. The program is not a snapshot that exists in a vacuum. Most programs are going to grow over time and have things added and removed in various places by many people. They're going to have many interfaces and operations.
I think you're arguing that tests and types can both be used to check a particular case for correctness. Sure, this is true. However "moving type checking code into the test suite" means nothing—that would just be type checking.
When you make a code change, there's a difference in the kinds of feedback you get from your tests and your types. Tests usually cover business logic or stories—things that you want or don't want. Types ideally cover everything. They check every operation applied to a given piece of data. Of course types are rarely precise enough that they can catch every logic bug (e.g. strings with semantics not encoded in types, like email addresses).
This is just scratching the surface. You might just have to try out both to get a better sense of how they feel to work with.
So at one of my older jobs, we worked primarily with C code that ran on a mini linux box inside a plane, and interfaces with a sensor pacakge. We wanted to make sure that the software was 100% correct cause any errors would mean an aborted flight test
We basically ended up creating a tool+language spec that would let us define the mapping of input to output sequences. We wrote it in such a way where we sat with scientists and pretty much mapped all the possible cases that they could think of for valid inputs and what the code should produce.
Then this tool would basically write automated tests for us, in such a way as to not only test correct behavior, but also do combinations of inputs out of order, fuzz testing, and so on. We ended up making it also check memory state, to ensure that there was no memory leaks, and analyze the memory space for required data or data that should not be there.
In the end, whenever someone was developing anything for this software, they would basically just run the tests, and it would be very good at catching possible errors, mostly on the negative side (i.e for a fuzzed input, it would result in an output that should be an error).
We could have done the same thing with a typed language, but it would have to be very strict typing to the point of something like CoQ, and it would have taken us probably the same amount of time to write that.
Hey, that's awesome. Seems like a great case for verifying things that way! I'm thinking of different cases I think, where you've got something like a distributed system or a web application and it's just harder to fuzz. But I agree, that seems a lot more practical than formally verifying it when that's the kind of testing you need.
Types [1] can only reason about categories of values, not about values. Tests and types do have an overlap, but the best option is both. Especially when combined with fuzzing, types can exclude large number of cases, making it even more efficient at covering a huge range of code paths.
[1] yeah, there are type systems like lean, coq that can do both, but the proving process is just currently not realistic for everyday applications
1. refactoring are in my experience still much faster (and reliable doable) with rust compared to e.g. Js/Python even in presence of a lot of tests. This is a bit less of an point with Java/TS/C# etc. through I had some very bad (and also some good) experiences with refactoring in TS. And to be clear I don't just mean pure refactoring but any larger changes affecting many places in code which might be needed to idk. impl. some feature.
2. especially with Js,Py and similar there are way to many edge cases you can have to test for all of them. Sure most times this mainly matters when writing libraries but on larger projects does apply too. Stupid stuff like you expecting a `list[int]` and someone (externally i.e. outside of your tests) passes a `dict[int, int]` and that happens to work as you current impl. is only linearly iterating it as if it's a `Iterable[int]` but then you change the impl to require a `Sequence[int]` as you access it by index in some corner case and now you customer has really strange subtle bugs. Can't be caught by your tests as the problem is the customer but still breaks the customer which is always bad and can't happen with rust. Sure also won't happen if everyone uses type annotations and mypy correctly and strictly. Through you can't rely on your customer using mypy, but you can rely on your customer running compiler checks (as it's the only way to build the code). Also while mypy is much much much better then pylance it is still prone to issues as both `cast` and `ignore[..]` are things you sometimes need but which easily can hide bugs if the code changes (cast doesn't pin the "from" type and ignore is scoped by place not by what is wrong)
Albeit it makes the process easier compared to a really shittly written code without strict typing, but against good codebases, it takes the same amount of time.