Conversely, it gives two opportunities to avoid not only typos, but "thinkos". Simple declarative definitions can often define the results of complicated algori

Conversely, it gives two opportunities to avoid not only typos, but "thinkos". Simple declarative definitions can often define the results of complicated algorithms. Algebraic topology is actually a nice example. Presumably a surface has no holes if and only if any loop on the surface can be contracted to a point (given appropriate definitions of all these terms, of course). While this equivalence is easy to verify, def has_holes(s): for c in all_loops(s): try: contract(c) except: return True return False isn't an effective algorithm (e.g., "all loops" is an infinite set). But algebraic topology shows how one might instead reduce the problem to computationally tractable linear algebra. Suppose, then, that you've implemented an (presumably nontrivial and therefore error-prone) algorithm to carry out this reduction. Then your patently correct constraint on all loops might be a useful source of tests. (disclaimer: I know nothing at all about computational algebraic topology, except that it's fascinating. So please take my example with an unbounded grain of salt.)