Spec#, nullables and more

[bearophile]

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

Bye,
bearophile