Sure, but static analysis can only add so much, as the programmer is still working in the base language and can't convey higher level concepts to the static analysis tool, so it's forced to backfit them by guessing intent. And to the extent you can make annotations for this, you're effectively working in a new formal language without the benefit of a compiler.