Andrei's list of barriers to D adoption

[Ola Fosheim Grøstad via Digitalmars-d]

On Wednesday, 8 June 2016 at 13:43:27 UTC, Timon Gehr wrote:
> On 08.06.2016 01:59, Walter Bright wrote:
>> ...
>>
>> I suspect D has long since passed point where it is too 
>> complicated for
>> the rather limited ability of mathematicians to prove things 
>> about it.
>
> The main reason why it is currently impractical to prove things 
> about D is that D is not really a mathematical object. I.e. 
> there is no precise spec.

Besides that, even if a @safe checker is slightly flawed, it only 
has to be vetted better than the backend which most likely is 
unverified anyway.

This is different from some of the static analysis done on C, 
which convert the LLVM bitcode or even X86 assembly into a format 
that can be queried using a solver. That way the proof holds even 
in the case where the backend is buggy.