[fredsir]

What you are saying is like the people that would "rather write new functionality than tests"... Like, yeah, that would be nice, if you were able to write 100% bug free code, but you aren't so your tests are actually important in the goal towards a working product.

[falcolas]

Well, I'd actually rather write unit tests than shake out type trees too, so no, the two statements aren't equivalent.

Why? Unit tests also check a lot more than the types being passed around, so they are a lot more useful in the long run. There are some type systems where this is perhaps not the case, but they certainly aren't the majority. The majority is "so do I go with a float or a double" or "I have to cast this int to an uint64 for this one function".

[lmm]

So use a good type system rather than a bad one. I mean if your point is "some popular type systems are so bad that they're worse than no type system at all" then I agree with you, but don't tar all type systems with that brush.

[fredsir]

A language that is exceedingly popular and has a great type system and has great tooling for tests is Rust. When using Rust, it’s quite evident why you have to use both and not one or the other.

And when it comes down to it, in theory, proofs are better than tests, and Id say no one would disagree, and in practice, types are proof. Unfortunately, you can’t use types for proving everything, so that is where tests comes in.

Imagine a platform where you could indeed prove everything. I believe, but am not sure, that there is some languages that do this, like Idris.