Take the example from the article. The contract trips at runtime, not at compile time.
There is a lot of interest in static analysis enforcing contracts, but this will likely require some additions to the contract specification.
> this will likely require some additions to the contract specification.
You need a lot more machinery to move this stuff to compile time, and not everything can be checked at compile time. The first example in the post would require you to validate that a <= v's len before indexing in order to be evaluated at compile time, for example. (Which of course is a runtime check anyway...)
By whole program analysis I mean you need the entire call tree of a function - stopping only when you can validate that the range of values is constrained to legal values. For some functions this is really simple, while for others the whole flow can be thousands of functions.