There's some truth in what you say, but there's a leap that we have not yet been able to make. The way I think of it, anyway, is that we'd like to specify just

There's some truth in what you say, but there's a leap that we have not yet been able to make. The way I think of it, anyway, is that we'd like to specify just the contract (preconditions and postconditions) of a module, and have an efficient implementation synthesized automagically (complete with well-designed submodules with their own contracts). That capability would be more than just another rung up the abstraction ladder. Interestingly, the problem of reasoning about programs at that level seems to be pretty nearly "AI-complete". This is true even though it's a formal domain -- one doesn't need, for example, the intuitions about the behavior of physical objects that we humans acquire through years of experience, nor an understanding of human behavior and emotions, etc. etc. We work pretty hard to make sure the behavior of a program is predictable just from understanding the program itself (there are occasional exceptions, of course). Yet even reasoning in such a restricted domain, about even very pedestrian programs, is beyond the state of the AI art at the moment.