[MattPalmer1086]

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.

Obviously, bugs which exist at a highér level than whatever automated correctness system you employ can't be handled by it and need something else.

I'm upvoting you, because while I don't agree with you, downvotes shouldn't be used to express disagreement.

[gvpmahesh]

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

ps: Thanks for the upvote :)

[MattPalmer1086]

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!