Andrei's list of barriers to D adoption

Timon Gehr via Digitalmars-d digitalmars-d at puremagic.com
Wed Jun 8 04:50:00 PDT 2016


On 08.06.2016 01:07, Andrei Alexandrescu wrote:
> On 6/8/16 12:53 AM, Timon Gehr wrote:
>> On 08.06.2016 00:47, Walter Bright wrote:
>>> On 6/7/2016 3:23 PM, Timon Gehr wrote:
>>>> Obviously they proved the virtual machine itself memory safe,
>>>
>>> As I recall, the proof was broken, not the implementation.
>>
>> Which time?
>
> That is an old result that has essentially expired and should not be
> generalized. See
> http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00849.html.

I think this can't be what Walter is referring to: "the type inference 
system for generic method calls was not subjected to formal proof. In 
fact, it is unsound,"

I.e. no proof, unsound.

> I assume the matter has been long fixed by now, do you happen to know?
> ...

I don't know.

BTW, Java's type system is unsound [1].

class Unsound {
     static class Bound<A, B extends A> {}
     static class Bind<A> {
         <B extends A> A bad(Bound<A,B> bound, B b) {return b;}
     }
     public static <T,U> U coerce(T t) {
         Bound<U,? super T> bound = null;
         Bind<U> bind = new Bind<U>();
         return bind.bad(bound, t);
     }
     public static void main(String[] args){
         String s=coerce(0);
     }
}


>>> People do
>>> make mistakes and overlook cases with proofs. There's nothing magical
>>> about them.
>>>
>>
>> Obviously, but there are reliable systems that check proofs
>> automatically.
>
> It is my opinion that writing off formal proofs of safety is a mistake.
> Clearly we don't have the capability on the core team to work on such.
> However, I am very interested if you'd want to lead such an effort.
>
>
> Andrei
>

I'll probably do it at some point. (However, first I need to figure out 
what the formal language specification should actually be, this is one 
reason why I'm implementing a D compiler.)


[1] https://www.facebook.com/ross.tate/posts/10102249566392775.


More information about the Digitalmars-d mailing list