Sun, 01 Aug 2010 23:33:38 +0000, retard wrote: > Sun, 01 Aug 2010 16:02:56 -0700, Jonathan M Davis wrote: > >> On Sunday 01 August 2010 14:13:40 Andrei Alexandrescu wrote: >>> Most languages have not been proven sound. I know ML has been, and >>> there is a reduced version of Java (Featherweight Java) that has been >>> proven sound. I know that Java with generics has been shown unsound a >>> long time ago >>> (http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/ > msg00849.html) >>> . I haven't followed to see whether that issue has been fixed. My >>> understanding is that as of this time Java with generics is still >>> unsound, i.e. there are programs without casts that produce type >>> errors at runtime. >> >> Thanks to reflection, it wouldn't be all that hard to shove the wrong >> type into a container with code that can't be properly checked at >> compile time. Since all the generic stuff is simply compile-time >> checks, the compiler fails to catch the problem, and all of the code >> which compiled with the assumption that the objects in the container >> were all of one type will fail when it goes to get the item with the >> wrong type out of the container. I think that all of the casts are >> still there though (since technically, the container holds Objects not >> the specific type). It's just that they aren't in the user code. >> >> In reality, this sort of thing pretty much doesn't happen, because you >> have to go out of your way to make it happen, but as far as proofs go, >> it's definitely going to fail. >> >> - Jonathan M Davis > > If you restrict yourself to a subset of the language with no casts and > no pointer manipulation, all kind of safety properties of the > polymorphic / generic containers can be proven. There is even a "safe" > version of casts known as pattern matching in languages like Scala. > However, if the class hierarchy isn't sealed, one cannot prove whether > the pattern matching function is total. There are also other issues with > patterns because of the type erasure in JVM. > > Sounds like Andrei might have read the brick wall book by B.P. It's a > basic book about language design (orthogonal to the parsing/backend > books like the one with the dragon in its cover) and an essential part > of grad/ postgrad studies in many places. It's a good read they say.
My bad, didn't open the link above until now.