"but easy for it to reason about the high-level semantics."
Is it? Does it make it possible to argue about such things as that mappings can be fused, for example? I keep wondering about the possibility of very-high-level algebraic transformations of programs (although admittedly, this could be shifted into some kinds of CASE tools instead).