TLA+, SPARK, Frama-C, PROMELA, Astree, even plain C or C++ and a heavily safety-oriented process are used when correctness is important more than any of the FP

TLA+, SPARK, Frama-C, PROMELA, Astree, even plain C or C++ and a heavily safety-oriented process are used when correctness is important more than any of the FP languages you've mentioned. In fact, by mentioning Erlang and Ericsson, you exhausted the only case supporting your point. Maybe if you tried hard, you could come up with a couple more. Now let's do the same exercise for the languages and tools I enumerated and it will take a long time until one runs out of examples. WhatsApp is another perennial example in these discussions. I can accept it although there's nothing critical about a chat app - and once again it's rather an exception instead of the rule. Most chat applications are written in "not FP" programming languages and work just as reliably as WhatsApp. In case it's not yet clear from the above, I believe that only tools which are used heavily in the industry deserve our attention, not obscure languages which haven't been put to the test and one off projects. The oldest trick in the FP argument book is finding some minor FP language to match any requirements put together by critics. So yes, I've heard of Idris and Agda - on HN - because barely anyone else uses them or talks about them. Coq is perhaps the outlier, because it was used to verify CompCert, but then again CompCert itself is used to implement a lot more things. But Coq, Idris, Agda and so on are actually red herrings, because when people praise FP's correctness benefits, they refer to standard languages like Haskell, F# or OCaml for which there is in fact little proof that they have a significant effect on program correctness. Obsessively encoding information in the type system will reduce or eliminate some types of errors, but that's far from proving a program correct and really not that far at all from what's available in other standard, mainstream languages, for less effort, better support and a great ecosystem.