Last May, I wrote about an article by Radu Grigore that claimed that “all Java type checkers have bugs”, and what that claim might have meant. Later, Grigore expanded his original short article into a full-length paper that appeared at POPL 2017 a few weeks ago. The appearance of “Java Generics are Turing Complete” at POPL made me go back and reconsider what I wrote last May, given the new version of the paper. It turns out that the new version revises the sentence I quoted at the beginning of my May 2016 post from
For Java, Theorem 1 implies that there cannot exist a formally verified type checker: All Java type checkers have bugs.
For Java, Theorem 1 implies that a formally verified type checker that guarantees partial correctness cannot also guarantee termination.