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.
