This is what&#x27;s usually called a &quot;liveness&quot; property: eventually the system will do some particular thing. These two in particular are often called &quot;progress&quot; in some contexts, but that&#x27;s rarely formal.<p>In general, any of these properties can be checked statically, just like czwarich said. You have to be conservative, but that&#x27;s not any different than a type system, or Rust&#x27;s borrow checker. There are certainly languages that enforce termination, and you can design systems that enforce higher-level progress properties (such as absence of deadlock).<p>The major difference between a liveness property and the other kind (called a safety property: at no point does this bad thing happen) is that you can&#x27;t check for liveness properties dynamically.