Poor man's runtime "dynamic" version. AKA: A much worse version.

In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.

"Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.

In other words: refinement types are a better solution.