Contracts are a good idea, but I find the implementation of them to be clunky. I'd much rather contracts be part of the type system than as function signatures. Using the example in your earlier link, instead of defining day's 1..31 range within the Date-struct invariant, you'd instead declare a "day" type that's an int whose value cannot exceed 31 or be less than 1. This would be checked and enforced anytime a variable of the type is [re]assigned, set as a field, or passed-in as a parameter.