It does run at compile time, and it doesn&#x27;t run afoul of Rice&#x27;s theorem (a useful generalization of the theorem about the halting problem) because it&#x27;s not implementing a general decision procedure that can decide for _all_ programs whether the property holds.<p>It&#x27;s possible to solve halting-class problems for restricted subsets of programs, as well as to enlarge those subsets greatly by forcing the user to help.  For example, I can trivially &quot;solve&quot; the halting problem for the subset of programs that contain no loops or recursion, by simply refusing to make a decision on programs that do.  I can also solve it for the subset of all programs that do halt by simply running the program and reporting when it halts that it does, in fact, halt.<p>More usefully, the type systems in Peaker&#x27;s examples rely on user-provided annotations to help the compiler &quot;see&quot; the truth of the user&#x27;s claims (or equivalently, the compilers restrict the class of programs they operate on to those programs which contain sufficient user-provided annotations).  The compiler doesn&#x27;t have to prove everything itself - it only has to check that the proof is valid according to the rules of the relatively simple logic of the proof system.<p>The history of type systems has largely been a story of improving these logics and inference systems to reduce the amount of help needed from the user and enlarge the class of things that can be proven about programs.  In this context, Rice&#x27;s theorem amounts to saying that, no matter how complicated you make your type system, there will _always_ be programs that either (a) are valid but not accepted, or (b) are accepted but not valid.