I'm glad you liked it! And note that even a proof doesn't ensure you're safe. There are actually multiple proofs that Java's type system is sound. The problem is they don't handle all of Java (can you imagine how many years that would take to do?), and for historical reasons they happen to not handle null. Consequently, all the proofs were correct, but they failed to model Java correctly and missed this bug. Validation vs. Verification, if you know the software-engineering terms.
As for the bug, you made me realize I wrote this version of the paper a little incorrectly. In the original paper, I made sure to emphasize that the type-checker was not to blame. The reason is that, even though the type-checker is rejecting some valid Java code, that's necessarily going to happen. Type-checking Java is undecidable, and so it's impossible for a compiler to be always right. Our examples happen to fit into the space where some compilers succeed and some compilers fail. So in fact the program should type check, but it seems harsh to blame a compiler for occasionally failing to do the impossible, especially when the JLS's suggested algorithm fails to do so as you have found!
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
I'm glad you liked it! And note that even a proof doesn't ensure you're safe. There are actually multiple proofs that Java's type system is sound. The problem is they don't handle all of Java (can you imagine how many years that would take to do?), and for historical reasons they happen to not handle null. Consequently, all the proofs were correct, but they failed to model Java correctly and missed this bug. Validation vs. Verification, if you know the software-engineering terms.
As for the bug, you made me realize I wrote this version of the paper a little incorrectly. In the original paper, I made sure to emphasize that the type-checker was not to blame. The reason is that, even though the type-checker is rejecting some valid Java code, that's necessarily going to happen. Type-checking Java is undecidable, and so it's impossible for a compiler to be always right. Our examples happen to fit into the space where some compilers succeed and some compilers fail. So in fact the program should type check, but it seems harsh to blame a compiler for occasionally failing to do the impossible, especially when the JLS's suggested algorithm fails to do so as you have found!