Tldr: a buggy imperative program can be mechanically translated into an equally buggy functional program.