Languages like Dafny and Ada show that you can contracts are great for augmenting a good type system by letting you express really complicated invariants that are tough to express in types. I didn't include them because they're not "mainstream", IMO.