The use of various forms of contracts, like preconditions, are increasingly receiving more attention within Microsoft. This talk describes the design of Spec#, an experimental superset of the language C#, including pre- and postconditions and object invariants. Spec# gives rise to dynamic checks of contracts. The contracts can also be checked statically using the automatic checker Boogie. The talk also reports on some initial experience and describes some difficult issues in the design.