Spec#, nullables and more

[Adam D. Ruppe]

Walter said:
> Couldn't this happen to you with any datum that has an unexpected value in it?

Yes, indeed. And being able to disable struct default constructors would (I
believe anyway) let us fix that in the library too, by forcing initialization upon
declaration.

Right now, we could write a struct that does runtime checks to ensure its payload
is always in range, with the exception of one line:

Bounded!(10, 100) myInt; // can't do the check

In this specific case, the bounded template could change the default
init value for its payload, arbitrarily picking some value in range. But you can't
do that with a NotNull struct - there is no default value that's usable, except
for null, which we're aiming to avoid!

If the default constructor were @disable-able, these structs could say:

Bounded!(10, 100) myInt; // compile error

Bounded!(10, 100) myInt = 10; // calls Bounded.this(10), passing the compile time
check, and allowing us to do the runtime check - it automatically runs the
struct's invariant!

The very same thing allows a not null struct - it forces explicit initialization,
which gives the invariant a chance to run, thus catching the error instantly at
runtime.


While compile time checks are probably more ideal, most of this works in the
language today, so I think it's a pretty conservative change that enables a few
simple library solutions to this whole range of situations.