I would love a language that distinguishes functions (pure mathematical constructs) from procedures (imperative constructs that map in a predictable way to the instruction set).

This feels like the direction Algebraic Effects might take us.