Coverage numbers are misleading (to the point that I find they did more harm than good). There are definitely cases where you can't (or aren't clever enough to) express what makes your business logic valid in the type system and need to write a test, but IME they're the exception rather than the rule (both because you generally can encode things in types, and because the majority of code ends up being "plumbing" with no real business logic anyway); I like to follow something like https://spin.atomicobject.com/2014/12/09/typed-language-tdd-... .
I like that article! It doesn't say to do away with coverage though, it simply talks about using good typing to make coverage easier to get with fewer tests. Like you said, sometimes you can't get the type system to enforce correctness, and sometimes you may think you have done so when you haven't, you always need tests to see.
I'm not sure what you mean by "coverage" - the article is advocating deleting (or not writing) tests if you can move the corresponding check into the type system, and the end result is that you will naturally end up with codepaths that aren't covered by tests (because those codepaths essentially "can't go wrong"). That makes the things that I've normally heard called "coverage" pretty useless.
