in some sense, strictly speaking they shouldn't be necessary, because the fact that my specification starts with an assumption, says, hey you, who might call square root, make sure that the things you call me with obey the assumption.