Andrei's list of barriers to D adoption

[Andrei Alexandrescu via Digitalmars-d]

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 assume the matter has been long fixed by now, do you happen to know?

>> 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