Axiomatic purity of D

[retard]

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.