I did some reading today about Agda, a dependently-typed language. I think there are some neat ideas in there.
For any declared contract requirement there are some contracts that could be checked statically and this should be done as much as possible in the programming system. This is going to be a similar job as the dependent type checker in Agda is doing.
Also it should be possible to determine statically in most cases when someone is trying to call a method that is not or may not be defined.
And, totality checking also is interesting and it would be nice to give an error if something is being called in a way that may run forever.
It would be very nice to have, for example, the ability to determine whether a list is empty or non-empty statically and allow the programmer to call a method to get the first element and know that they'll get an error from the analyser if they may have made a mistake.