So long as the problem you are trying to solve is constrained by the ease with which you can express the problem, this will help.
But it will not help when the constraints are elsewhere: memory, network, CPU, heterogeneous interoperability; all still relevant in these times of mobile and distributed computing. When you are operating to these other constraints, you need control - or rather, consistency and predictability - over the consumption of those other resources. It's no good having a magic compiler that can turn your specification into an implementation, if you don't know whether the implementation will run in O(1) or O(n) space or time, what kind of constant factors are involved, and how easily you can tweak the tradeoffs when you hit one constraint or another.
I concur with raganwald's comment: this is more useful for proving, static analysis, testing, etc.
Furthermore, I'm pessimistic that you'll see substantial improvements in expressibility using your approach, particularly when you try to scale it above simple functional (by which I mean stateless input to output) problems. The reason is that programming is an exercise in attention to detail while simultaneously keeping the large in mind; and your focus won't change this fundamental nature. Writing a complete specification for a program rivals writing an imperative implementation in complexity (soup to nuts, I'm not talking about high-level DSLs here, which is an approach equally applicable to the imperative route). I expect a good compiler will swamp you with the inconsistencies of your hidden, unstated assumptions.
For example, I note that your sorting specification doesn't specify whether or not the sort is stable; I think that makes it incomplete, and also it's a tricky constraint to encode.