It's not significantly different from describing correctness in, say, tests written in the same language. By doing something twice, you would have to make the s

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