There are sound static analyzers, like Trust-in-Soft, that can statically guarantee the absence of undefined behaviors in C programs, but require interactive wo

There are sound static analyzers, like Trust-in-Soft, that can statically guarantee the absence of undefined behaviors in C programs, but require interactive work to get rid of the false positives. But the distinction between "runtime" and "compile-time" is not entirely binary. What you call "compile time" checks can be viewed as an abstract interpretation [1] of the program, or as running the program in some abstract domain -- e.g., where a concrete value could be 3, its abstract value could be called `int`, and the + operation could be interpreted as `int + int = int`; type inference could be viewed as abstract interpretation. The problem is that sound abstract interpretation (i.e., one without false negatives -- if it tells you your programs is "safe" then it will definitely be safe, for some appropriate definition of safe) is limited, and often comes with big tradeoffs, e.g. either false positives given by sound static analyzers or the pain something like Rust's borrow checker sometimes causes -- these are both instances of the same underlying difficulty with abstract interpretation. One of the most promising directions in formal methods research is "concolic testing" [2], which means a combination of concrete (i.e. non-abstract, or "runtime") execution and symbolic execution (an instance of abstract interpretation). It is not sound, but can be made quite safe, and at the same time it can be very powerful and flexible, checking properties that can be either impossible or extremely tedious, to the point of infeasibility, with abstract methods like types. It might prove to be a good sweet spot between the power, expressivity and cost of concrete (AKA dynamic, AKA runtime) methods and the soundness of abstract (AKA static, AKA compile-time) methods. Even dynamic methods are often "stronger" (more sound) than just testing assertions during testing. For example, fuzzers can sample the program's state space, offering more coverage, either by analyzing the program (whitebox) or just randomly (blackbox), and various sanitizers sample the scheduling space by fuzzing thread scheduleing. [1]: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation [2]: https://en.wikipedia.org/wiki/Concolic_testing https://en.wikipedia.org/wiki/Concolic_testing