I'm a bit confused - they recently discovered Java is unsound? I thought this was well-known for quite some time because of broken co/contravariance?

On recent Java developments, Java's undecidable typechecking has now been proven:

http://dl.acm.org/citation.cfm?id=3009871

I hate to be that guy, but in the fourth paragraph, the author mentions the variance issue as old news.

Main discussion here: https://news.ycombinator.com/item?id=13472553

This does do a better job of laying out the reasoning for those less apt at reading academic proofs.

It's a good root cause analysis.