Andrei's list of barriers to D adoption

[Walter Bright via Digitalmars-d]

On 6/7/2016 4:01 PM, Jonathan M Davis via Digitalmars-d wrote:
> Yeah. I recall an article by Joel Spoelsky where he talks about deciding
> that proofs of correctness weren't worth much, because they were even harder
> to get right than the software.
>
> I do think that there are situations where proofs are valuable, but they do
> tend to be very difficult to get right, and their application is ultimately
> fairly limited.

My understanding is that academic researchers who need to prove a theory use a 
subset of Java, because the smaller the language, the more practical it is to 
write proofs about it. I also remember bearophile bringing up the Spec# language 
which was supposed to be able to formally prove things, but it turned out not 
much. I fed it some one liners with bit masking which it threw in the towel on.

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.