Confidence in a program's behaviour is not an all-or-nothing proposition. You can statically verify certain properties of your program (through immutability, ty

Confidence in a program's behaviour is not an all-or-nothing proposition. You can statically verify certain properties of your program (through immutability, type systems, linters etc.) without having to write a full formal proof of your program's entire behaviour, and you can gain more confidence in the entire program working correctly. In the example you just gave (summing over a list of numbers), in almost all programming languages you'd resort to runtime verification instead, i.e. tests, just because it's so much more practical. But if you have a PFP language, you still have the confidence that the behaviour of the inputs and outputs is the only thing you have to test, since the function cannot do anything else.* Even in a non-pure FP language, you know that it cannot mutate other variables, although it might have side effects. * Ok, it might loop forever or crash, but that's comparatively rare.