Agree on the economics. I’m not arguing for full formal proofs; I’m arguing for low-cost enforcement of invariants (ADTs/state machines/exhaustiveness) that makes refactors safer and prevents silent invalid states. Human processes will always drift, so you enforce what you can at the system boundary and rely on reconciliation/observability for the rest.
In the banking subdomain of credit/debit/fleet/stored-value card processing, over time when considering regulation and format evolution, services provided by banks/ISOs/VARs will effectively exhibit FP traits regardless the language(s) used to implement them.
Savvy processors recognize the immutability of each API version published to Merchants, along with how long each must be supported, and employ FP techniques both in design and implementation of their Merchant gateways.
Of course, the each bank's mainframes "on the rails" do not change unless absolutely necessary (and many times not even then).