I think the main difference between assertions and static type-checking is that ... static checking can do its checks at compile time. That is a great feature f

I think the main difference between assertions and static type-checking is that ... static checking can do its checks at compile time. That is a great feature for big projects. But the benefit of assertions is they can express arbitrary requirements, not only about the type of each argument and result but also about intra-arguments relationships between arguments, and also between arguments and the result. As an example I could say: ok (argA < argB); ... ok (result > argA - argB); It's a tradeoff: More expressivity, simplicity and speed of development vs. earlier detection of type-errors.