[whatshisface]

In the logical extreme that can't be the case, because a fully debugged program plus a machine to run it on actually satisfy the definition of a formal specification. Deciding what you want your program to do is the eternal burden of programming, but maybe there's a way to make formal specification at least as easy as regular programming.

[adrianN]

But then you already have a perfect implementation that you somehow made without the use of formal verification. But you want to introduce formal verification because translating real-world requirements into a formal language is hard enough that you can't be sure of correctness...