If I have a Vector3.Normalize() method that specifies a post condition where the resultant Vector3 is gonna have a length of 1, how would the compiler check for this at compile time (or before)? Does it just pass a random Vector3 variable to the method?
This isn't a feature of C# 4.0. It's a language-independent feature of CLR 4.0 that works at the IL level. It does have some ability to perform static checking, but not for every kind of condition. It actually analyzes the IL generated by the normal compiler for whatever language you're using, finds the constraints you put in the code and then looks at the code to figure out if it is going to meet the contract. The static checking (at least in demos I've seen) is an optional feature.