Spec#, nullables and more

[Walter Bright]

bearophile wrote:
> Walter Bright:
> 
>> Adding ranged integer types increases the coverage from 1% to 2% of the
>> cases. (Pulling random numbers out of the ether, but still, I think the
>> point is valid.)
> 
> I don't know if that point is valid. SPARK language is able to have a
> testable low bug count, and it only has nonnulls and ranged integers. But it
> also uses other unrelated features, like a very precise and defined
> semantics, design by contract enforced statically (like Spec#), all functions
> need to list what outer variables are able to see, plus it has few other
> safety features (like not allowing recursion, restricting pointer usage a
> lot, and so on). So despite SPARK doesn't seem to need more than those two
> kinds of value constraints (nonnulls and ranged integers) I don't know how
> many bugs those two features alone avoid and how many are left to be caught
> to the other safety features. My hypothesis is that those two often suffice.
> But indeed I can't be sure. In an ideal world I'd like to add them to D and
> then use D for few months and see how much less bugs I put in my code (I keep
> an updated list of all my bugs).

Very, very few (if any) dmd issues on bugzilla would have been caught by ranged 
integers or non-null pointers (despite there being several seg fault bugs).

The vast majority of the problems were the result of an incomplete understanding 
of how things should be done, rather than a coding error. (A coding error being 
things as simple as a typo or forgetting to initialize something, aka "stupid 
mistakes".)

I think that's in no small part due to my programming for a very long time, and 
I've developed all kinds of strategies for avoiding the "stupid mistake" kinds 
of coding errors.

As Andrei suggested out to me, and I agree, the notions of non-null types, 
ranged integers, and the like's primary advantage is not in reducing the bug 
count, but in enhancing the self-documenting nature of the code. It makes the 
code easier to reason about, and easier to modify.