> This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the s

> This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the spec. This seems to ignore a vast majority of possible software. It's easy to confirm/test whether a function, with no state, takes a certain input and produces a certain output. You can write that in a spec. You can unit test that. But that ignores the whole concept of state; the whole state of the system. If X happened yesterday, Y happens now, and X and Q are true, and it's a Wednesday and a full moon then the output is Z. By the time you've encoded that and every other variation into a spec, congratulations you've written the software!