Took type system and advanced compiler last year. This paper may not look very interesting but there are a lot of proof assistant softwares that verify featherweight Java's type system to show that they work. This paper also shows that there are a lot holes in Java type system even by 2002 that makes it broken. Java's type system is probably much worse now. I think it also started the trend of featherweight-X where you try to proof a subset of a language X type system to show that if you take away features y,z and etc then type system can be proven.