Yeah, I imagine the formal logic being quite strict, maybe requiring formal verification. It wont stop business-leaky-cases, but it might give us something deterministic that is better than what we have - we dont need perfection, an order of magnitude (or 5) jump in productivity would do...
We've tried. The problem with layers of abstraction is that they're leaky, and don't always work.
For example, simple SQL is easy. Optimizing SQL requires intimate knowledge of your db engine.