If we want zero-overhead abstraction (i.e. don't generate null checks in front of every division, etc.) and a (reasonably) safe language, more static analysis i

If we want zero-overhead abstraction (i.e. don't generate null checks in front of every division, etc.) and a (reasonably) safe language, more static analysis is in order. The case in point is Rust: Its type system is basically an elaborate static analysis. Rusts advantage over tools like UBsan is that the programmer expects to interact with the type system. Many static analysis tools get rejected by programmers, because the expectation is that they "just work", when really one needs to interact with such a tool. This means bidirectional communication: The programmer tells the tool what invariant he wants to get, and the tool tells the programmer which invariants it is missing.