In Spec# they used MyRefType! (exclamation suffix) to mean non-nullable; so the default is wrong but they were aiming at backward compatibility with C#, so they had to go that way. And then they would just look for an if (myVar != null) and silently make myVar non-nullable within the truth block.
It looks like the closest we'll get to this in real C# is the Code Contracts library in CLR 4.0, but I really wish non-nullable was the default. Unfortunately it complicates the syntax in some areas (where should non-nullable instance fields in a class be initialized?) but it would surely have been worth it, as Hoare says.