I last touched formal verification methods 20 years ago. Back then, Coq had the capacity to automatically transform your proof into OCaml. I would have expected that this would have only gotten better with time.
It seemed to me from the survey that most people didn't want it changed or didn't care, but due to anglophone users they decided to change it anyway.