[wolfgke]

The problem is that most people are simply incapable of giving correct specifications.

In a lecture about this topic (how to create specifications that can be turned into formal correct code) we were given the following simple example of an incorrect specification:

"Everybody loves my baby. But baby loves nobody, but me."

If you formalize this, you can simply conclude that the person that says that is equal to the baby - which clearly is not, what you intended.

And this is a very, very simple specification. Specifications of real software are magnitudes more complicated.

[seanmcdirmid]

That is why the computer must hold a two way conversation with the programmer. How often do we just type out a program from our head to the computer anyways? Most of us write the program, debug it, change it because the result wasn't right, or we didn't really understand what we wanted, or someone else decided the requirements changed, or whatever...