1. 6

Important quote:

What is the practical relevance of Theorem1? For C, there exists a formally verified type checker in CompCert (Leroy 2009, version 2.5). For Java, Theorem 1 implies that a formally verified type checker that guarantees partial correctness cannot also guarantee termination. In most applications, partial correctness suffices, 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).