Peter Madden) (by way of Duncan Frissell <madden@mpi-sb.mpg.de> writes:
The real problems lie with specifying the program/problem correctly in the first place (so-called specifications capture), and with automatic program *synthesis* from specifications (which, in mathematical theorem proving terms, presents the problem of creating existential objects, as opposed to just verifying that they do the right job).
Bugs in specifications are just as easy for humans to produce as bugs in implementations, and unfortunately there is no way for our machines to psychically intuit what it was we wanted to specify that they do any more than we can make them intuit what it was we wanted them to do. Remember, by the way, that in some sense a high level programming language *is* a specification language. Authomatic synthesis from "specifications" is just a higher level of programming language, with all that entails. Perry