Formal specifications can do all that if you build thetoing for given language and platform. Static typing is a subset of formal specifications. I suggest using

Formal specifications can do all that if you build thetoing for given language and platform. Static typing is a subset of formal specifications. I suggest using the other phrase so they find more interesting stuff. Meyer's Design-by-Contract is an easy one you can do in basically any language.