I really wouldn't underestimate this. Formal proofs and verified programs pretty much always involve functional languages at the core because there's just less going on to complicate the proof. Once you start introducing state, manual memory management, unrestricted recursion, pointers, undefined behaviour etc. it becomes much, much harder to write proofs about programs and justify why they're bug free. This also carries across to humans...it's much easier to reason in your own head why a program is correct when the program behaviour is simple.