A type system and static analysis certainly allow you to stop writing a certain category of test as you no longer need to assert that a method being passed an object of the wrong type copes with that. It doesn't completely relieve of you the need to test though as a type system won't assert that the code you're writing actually fulfils the businesses requirement that nothing can be ordered for same day shipping after 11am.

You absolutely can do that with the type system, use a constrained subtype.

You've got my interest piqued now. How does that work in practice? And do you not still need to test that it complies with the actual business rules at some point?

How does that confirm to you that, say, your ratelimiter code is correctly processing the first three requests in a given minute, rejecting the fourth, and approving a fifth once another minute has passed?

But only tests will tell you you are calculating something correctly.

But thats anathema to agile, yo. /s