[voxcogitatio]

There is also the matter that the whole "correctness vs. productivity" debate is a false opposite. There is nothing mutually contradictive with correctness and productivity, so there is no reason why you can't have both.

[prodigal_erik]

Correctness stems from expressing not only the algorithm but also the results you expect from running it (as types and/or test cases) so they can be verified. But if you somehow convince yourself that you haven't made any mistakes, it's always less work to just write the algorithm (and omit the expected results).