I really like this idea. You'd essentially have to describe the same system twice, from two angles, and the compiler cross-validates them. This is more work, but I think this will help humans understand what it does, and what it is supposed to do better as well.

And it would aid maintenance/refactoring. Behavior that is now implicit in the code would have to be written down explicitly (separating desirable behavior and side effects/bugs), and unlike "design documents" it is actually validated... (ie, a refactoring would be changing representation 1 without changing representation 2)

Separating intent and implementation, so to say. You might be on to something.