[the_af]

Of course not everything can be encoded in types, and also YMMV regarding the specific language you're using.

But you now why I asked the question: people who make claims like "types make only guarantees about the type of values" usually don't understand what modern type-checking can do or what can be encoded in types. People making these claims often believe type-checking is limited to validating that you only pass strings to a function expecting a string argument, or some minor variation of that.

[gleenn]

The fact remains that your type system can be turing-complete and still not validate the actual logic that I need checked/tested.

[the_af]

The same can be said of tests.

Types are just tests. By removing all the mindless, repetitive tests you write, typechecking can free you up to write the actual meaningful tests that you truly need to write.

It's not "pick one", it's "use type checking to help you only write the unit tests that matter".