A few days ago, my friend Stephen Tu pointed me in the direction of “Java Generics are Turing Complete”, a “short note” that Radu Grigore recently posted on arXiv. In it, Grigore shows that in Java, subtyping is undecidable (his “Theorem 1”) and that therefore, type checking is undecidable. He then remarks:
For Java, Theorem 1 implies that there cannot exist a formally verified type checker: All Java type checkers have bugs.
Stephen wanted to know what exactly the claim of “all Java type checkers have bugs” meant. To understand what this means, let’s take a closer look at Grigore’s result.