Thanks for your perspective.
I'm wondering how this squares with the tendency of formal language theory folks to push for functional languages. It's clearly a preferred approach if rigorous correctness is your main goal, but don't functional languages like Haskell suffer from the fundamental issue that reasoning about runtime performance is really hard?