Earlier quoted context omitted.
I'll say that any unit test for a bug which would have been caught by a more sophisticated type system is a waste. I don't know how much time people spend writing such "obsolete tests", but I doubt it's insubstantial.
The problem is that sophisticated type systems only catch a subset of the bugs that a unit test can catch. For example, let's say I'm adding the ability to transfer funds from one account to the other in a banking application. I want to display a warning when the amount of money being transferred is over a certain percentage (let's say 95%) of the funds in the account. That's pretty easy to do in a unit test: create…
You could use Coq, Isabelle, or Lean. Their type systems are powerful enough to allow such checks.