Does this logic not basically invalidate anything that isn't imperative at a high level that eventually runs on a processor? Like, "why bother writing Haskell? It just gets compiled and ran imperatively." Isn't the whole point that you can reason about Haskell?