> a static analyzer can easily make sure that all function calls satisfy the contract

How realistic is the "all function calls" part? Maybe I just don't see the bigger picture, but I would expect most function calls arguments to only be known at runtime, which of course makes static analysis not possible?