Even simple type systems like in Java can help with correctness. For example if you have a list of "Person" but the code itself assumes it's a unique list of people you can convert that list to a Map<PersonId, Person>. Further if the map is assumed to never accept null values for either key or value you can capture that in some kind of "People" class that enforces invariant assumptions.
You're right that is does not prevent actual logic bugs but in practice, a lot of bugs are sometimes caused simply by bad inputs. With types you can make it so that logic never gets bad input eg (sqrt(NonNegativeDouble) instead of sqrt(double)) can potentially eliminate some error handling code.
I disagree strongly that types have nothing to do with correctness. Primitive types will only give you a limited utility, more complex type systems give you a lot more.
I agree that types can help with sanity of data flowing in and out, but how do you check the correctness of program with types?
Example: your function is doing some complex calculation, while the inputs types can be strongly checked and output types can be checked, but the logic has to be tested by writing unit tests right?
The original comment which i replied to suggests that we can get rid of TDD only if we employ using type systems, which i feel is over exaggeration of the benefits of the types
Yep, nothing gives you complete assurance of correctness. Even formal methods can have bugs in the specification.
It's good for the compiler to provide correctness guarantees where it can, but tests find different bugs. I think they are useful things to have.
Having said that, I once did an analysis of tests vs bugs in a fairly large code base. There was almost no correlation between number of tests and number of bugs.
Most bugs caught in the wild were actually failures of the developer to fully understand the spec. We had tests that enforced the incorrect understanding!
You're right that is does not prevent actual logic bugs but in practice, a lot of bugs are sometimes caused simply by bad inputs. With types you can make it so that logic never gets bad input eg (sqrt(NonNegativeDouble) instead of sqrt(double)) can potentially eliminate some error handling code.