Even if this were true my point (2) still stands. But it really isn't true because spec is part of the code. If your formalism is wrong, irregardless of whethe

Even if this were true my point (2) still stands. But it really isn't true because spec is part of the code. If your formalism is wrong, irregardless of whether implementation is correct, your code will behave wrong. There is absolutely no goal post moving. If my program is wrong, I can't tell my user "well, my unittests are all passing and I have 100% code coverage".