Summary: The BCL specification fails to specify that String.Empty is not null
Nearby: KnownBugsOrProblems, HomePage

Repro

Current behavior:

		 static class Test
		 {
		    static void Main()
		    {
		       string s = string.Empty;
		       assert s != null;  // Fails!
		    }
		 }
	

Expected behavior:

		 static class Test
		 {
		    static void Main()
		    {
		       string s = string.Empty;
		       assert s != null;  // Passes!
		    }
		 }
	

Explanation

The declaration of string.Empty is as follows:

		 // mscorlib.dll
		 namespace System
		 {
		    class String
		    {
		       public static readonly string Empty;
		       // ...
		    }
		 }
	

Discussion

I believe the way to specify that string.Empty is not null is through a static class invariant on class String, rather than by giving it a non-null type.

See K. Rustan M. Leino and Peter Müller, "Modular verification of static class invariants", FM 2005, http://research.microsoft.com/~leino/papers/krml153.pdf.

I don't believe that support for static class invariants has been implemented yet (as opposed to support for object invariants, which has).

Applying a non-null type to String.Empty would be problematic, because more generally allowing non-null types to be applied to static fields is problematic. This is because it is problematic to keep code from reading the field before it is initialized by the static constructor (short of disallowing any method or constructor calls before the fields are initialized, which would rule out many important patterns). This differs from instance fields because in constructors, calls may be allowed provided they do not take "this" as an argument. Also, instance fields may be initialized using constructor parameters, whereas static constructors have no parameters.

In this particular case, consider the following fictional code for class String:

		 class String
		 {
		    public static readonly string! Empty;
		    static String()
		    {
		       Empty = new String(new char[] {}).Intern();
		    }
		    public String(char[] chars)
		    {
		       int n = Empty.Length;  // Would the type system allow this?
		       //...
		    }
		 }
	

A non-null type system that allowed non-null static fields would have to deal with the above case.

I believe the current thinking in the Spec# team is that non-null static fields will not be allowed.