The example given with acceleration, velocity, and position? How is a compiler going to deal with that? With an Euler integrator, you say? (every frame, p=p+time_scaled(v), v=v+time_scaled(a) ). Note there's an implied time, as well as frames per second, in there, but a compiler can know about time. Unless when you're saying "acceleration" you're not talking about real time, but calculating where something will be at…
So when you've got to write a sort, you probably start in our hypothetical dream language by saying:
"sort permutes a list so that a Now "permute", with predicates, is probably built into the system and the constraint solver probably turns this into a variant of bubble sort, O(n^2). [That is, when you now query list[0] it does a reverse bubble-sort by looking for the least element rather than the greatest element, moving that to the lowest position.]
Now you come into this and say "hey, I've got a huge list, I need O(n log n) power." What do you use? Perhaps merge sort.
"sort zips together, least-element first, the sorted first half of input and the sorted second half of input -- unless len(input) If you can establish a consistent syntax for these sorts of claims which a constraint solver can follow, then the simplicity of the constraint solver, and your ability to guess what it will do, will allow you to determine which algorithm you use to perform the same task.
So it doesn't require strong AI and the programmer is still making the choice -- that's what I'm trying to say. The programmer is merely making the choice in a different framework: rather than making the choice in some wrapper for blocks of assembly language, you are making the choice in some wrapper for a constraint solver.
Now let me turn from where I think you're wrong to where I think you're right: I have the feeling that you're going to see something less revolutionary than claimed, because it will be like C's inline assembler support; in this hypothetical language you can probably "drop back down" to the pre-constraint-solver level when you can't figure out how to articulate the problem with constraints. (Something like "The constraint is, it has to come from applying this function to those lists!")