not only that, but what all of this misses is the fact that the specification that they used was a product of writing the software, not the other way round. It

not only that, but what all of this misses is the fact that the specification that they used was a product of writing the software, not the other way round. It would be much, much more difficult to first write a correct specification than to first write a correct program, because programs are formal systems that can be executed to observe their correctness. You can’t do that with a specification.