It&#x27;s not significantly different from describing correctness in, say, tests written in the same language. By doing something <i>twice</i>, you would have to make the <i>same</i> mistake for it to sneak through.<p>The specification is also easier to write because you don&#x27;t have performance constraints and you&#x27;re using a different set of abstractions than your main code.