When I see rust code I have the feeling that as a developer you are in a constant battle with the compiler to fulfill its type system.
I wonder if some unit test / fuzz tests in a less strict language could lead to the same amount of code quality yet at a higher level of work satisfaction while writing the code.
In my experience, types which prove certain properties are usually a lot simpler than the tests verifying the same (at least tests which actually have a good chance of catching transgressions, instead of just checking a single hard-coded input). So more expressive type systems bring me a higher level of satisfaction, because they lead to simpler code than the code I'd need to write if I needed to test the same things. They also provide valuable documentation. On the other end of the spectrum, when I look at untyped Python code, I feel completely lost and find myself scouring the documentation for information that should be obvious from function definitions, but is instead specified in prose 3 links away from documentation of the function I was interested in.
Types guarantee properties over the full set of possible inputs before you run any code. If you can enforce a property with a type, it is IME far less work than trying to enforce that property with a test.
"Less strict" inevitably means not caring about a bunch of edge cases. It's a bit like "overflow is undefined behavior in C"; nobody wants to care about how "i++" is a statement that's (a) absolutely everywhere and (b) potentially invokes undefined behavior at runtime, so the only way to guarantee that out involves a lot more proof work somewhere.
> If you can enforce a property with a type, it is IME far less work than trying to enforce that property with a test.
That's an unnecessarily broad generalization to a concrete statement, and if it were true more people would write their programs in dependently typed programming languages or whatever.
> nobody wants to care about how "i++" is a statement that's (a) absolutely everywhere and (b) potentially invokes undefined behavior at runtime, so the only way to guarantee that out involves a lot more proof work somewhere.
In many domains, the high standards you're displaying here will almost immediately throw you out of business.
In particular "i++" for most applications is just fine to write without any second thoughts. It's not even a good idea to write a test. Just run the program and fix it in the rare case something it doesn't work as expected (it's almost a safe bet the issue won't UB).
You're not taking a tank to go to the supermarket either, are you?
> more people would write their programs in dependently typed programming languages or whatever.
Programming language choice is greatly influenced by ecosystem factors. If you wanted to write a program for the browser, you had to write it in Javascript - so people went to considerable lengths to fit typed front ends onto Javascript.
> Just run the program and fix it in the rare case something it doesn't work as expected (it's almost a safe bet the issue won't UB).
> You're not taking a tank to go to the supermarket either, are you?
No, but if you're going into a live fire hostile environment you might want a tank, and the internet is such an environment. If there is a bug in your parser, and the parser is exposed to untrusted data, then that's a potential avenue for exploit.
Less of an issue in managed-runtime languages, but it's still possible to have semantic level exploits. I remember there was one for Apple which exploited the fact that there were different proplist parsers. https://daringfireball.net/linked/2020/05/02/psychic-paper
The idea of fighting ("[being] in a constant battle with") the compiler seems weird to me, the compiler is my automated helper, the stricter it is, the better I work and I thank it for correcting me.
I wonder if some unit test / fuzz tests in a less strict language could lead to the same amount of code quality yet at a higher level of work satisfaction while writing the code.