What is the practical relevance of Theorem1? For C, there exists a formally veriﬁed type checker in CompCert (Leroy 2009, version 2.5). For Java, Theorem 1 implies that a formally veriﬁed type checker that guarantees partial correctness cannot also guarantee termination. In most applications, partial correctness sufﬁces, but not so in security critical applications (where users are malicious), nor in mission critical applications (where nontermination is costly). Since there cannot be a totally correct Java type checker, Theorem 1 strengthens the motivation behind research into alternative type systems, such as (Greenman et al. 2014) and (Zhang et al. 2015).