First of all, I certainly appreciate your work. It's never safe to assume that something works without having some proof to back that up.
Regarding the correctness of the compiler on the first example, I will point you to the Eclipse bug report I filed where Stephan Herrmann explains it why this should not compile according to the JLS: bugs.eclipse.org/bugs/show_bug.cgi... It seems like there are multiple versions of the JLS in use by the different compilers, and that is the one of the reasons for the discrepancies.
I like the last example with the use of an Interface to hide the broken implementation, very clever. Just goes to show that you need to verify that your 3rd party libraries don't have bugs.
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.
First of all, I certainly appreciate your work. It's never safe to assume that something works without having some proof to back that up.
Regarding the correctness of the compiler on the first example, I will point you to the Eclipse bug report I filed where Stephan Herrmann explains it why this should not compile according to the JLS: bugs.eclipse.org/bugs/show_bug.cgi... It seems like there are multiple versions of the JLS in use by the different compilers, and that is the one of the reasons for the discrepancies.
I like the last example with the use of an Interface to hide the broken implementation, very clever. Just goes to show that you need to verify that your 3rd party libraries don't have bugs.
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!