Yes, I agree. The real test of AI is not the automation of “formal specification → working code”—if the client could formalize it to that level, they could write the code themselves. Rather, the real test is whether an AI could talk to an extroverted MBA, figure out what they want, and then produce the working code. But so far, only humans programmers can do that.
And by the same token, we’ll know we’ve nailed AI not when we have written a program that can have that conversation… but when we have written down an account of how we are able to have that conversation, to such a level of detail that there’s nothing left to explain.
Writing a program which solves the Towers of Hanoi is not too hard. Proving, given a formalization of the ToH, various properties of a program that solves it, isn’t too hard. But looking at a bunch of wooden disks slotted on pegs and coming up with an interpretation of that situation which corresponds to the abstract scheme we know as “Towers of Hanoi”… That’s where the fun is.
Yes, I agree. The real test of AI is not the automation of “formal specification → working code”—if the client could formalize it to that level, they could write the code themselves. Rather, the real test is whether an AI could talk to an extroverted MBA, figure out what they want, and then produce the working code. But so far, only humans programmers can do that.
And by the same token, we’ll know we’ve nailed AI not when we have written a program that can have that conversation… but when we have written down an account of how we are able to have that conversation, to such a level of detail that there’s nothing left to explain.
Writing a program which solves the Towers of Hanoi is not too hard. Proving, given a formalization of the ToH, various properties of a program that solves it, isn’t too hard. But looking at a bunch of wooden disks slotted on pegs and coming up with an interpretation of that situation which corresponds to the abstract scheme we know as “Towers of Hanoi”… That’s where the fun is.
One can’t proceed from the informal to the formal by formal means. Yet.
(Apologies to Alan Perlis etc)