3 ms·

Functional programming has no relevance to the correctness of code. You'll notice that it's virtually unheard of to use any FP languages in critical software.

by blub 8y ago

Functional programming has no relevance to the correctness of code. You'll notice that it's virtually unheard of to use any FP languages in critical software. Instead they use languages that lend themselves well to code reviews, static and dynamic analysis, model-based design and proofs, etc. Like C, Ada and some domain-specific stuff. The kind of "correctness in the small" offered by Haskel through its type system can be obtain also in languages like C++, Swift and others. With the additional benefit of massive market share, teaching resources, mature tooling and so on.

tombert 8y ago
>You'll notice that it's virtually unheard of to use any FP languages in critical software. Erlang powers around 40% of the world's phone networks; and if it's not mission-critical I'm not entirely sure what is. For that matter, Whatsapp is also written in Erlang and Jane Street does trading applications in OCaml. Without making a judgement on whether or not they should, both Whatsapp and Jane Street create very large apps and have created successful businesses with FP. > Instead they use languages that lend themselves well to code reviews, static and dynamic analysis, model-based design and proofs, etc I can't tell if you're being serious; are you suggesting that Functional Programming doesn't lend itself to proofs? Really? Have you ever heard of Coq or Idris or Agda? They literally have modes to prove the correctness of your code. What about functional programming doesn't lend itself to code reviews? I did F# for a living for two years and we had regular code reviews. I also used the .NET performance profiling tools which worked fine for F#. > The kind of "correctness in the small" offered by Haskel through its type system can be obtain also in languages like C++, Swift and others. Uh, no. Sorry, that's just flatly wrong. Yes, static analysis tools are awesome, but you will never get the same level of compile-time safety from C++ that you will from Haskell or Rust or any number of functional languages. The type systems offer very little information, making it impossible for the compiler to shield anything.
- blub 8y ago
  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.
  - tombert 8y ago
    I don’t know anything about SPARK or FramaC, but TLA+ isn’t a programming language, and you can use it to model distributed functional apps just fine (I still do). Even if the Erlang/Ericsson stuff is the “only case” (It’s not) I do not see how that makes my point less valid; Erlang was specifically design for systems that cannot fail. Telephones are just a good example of that.
    - blub 8y ago
      And doesn't your TLA+ model make your functional code significantly more reliable? Guess what, it does the same thing for OO languages => no need to use FP to increase reliability. Same goes for the other tools or languages I mentioned.

by blub 8y ago

tombert 8y ago

>You'll notice that it's virtually unheard of to use any FP languages in critical software. Erlang powers around 40% of the world's phone networks; and if it's not mission-critical I'm not entirely sure what is. For that matter, Whatsapp is also written in Erlang and Jane Street does trading applications in OCaml. Without making a judgement on whether or not they should, both Whatsapp and Jane Street create very large apps and have created successful businesses with FP. > Instead they use languages that lend themselves well to code reviews, static and dynamic analysis, model-based design and proofs, etc I can't tell if you're being serious; are you suggesting that Functional Programming doesn't lend itself to proofs? Really? Have you ever heard of Coq or Idris or Agda? They literally have modes to prove the correctness of your code. What about functional programming doesn't lend itself to code reviews? I did F# for a living for two years and we had regular code reviews. I also used the .NET performance profiling tools which worked fine for F#. > The kind of "correctness in the small" offered by Haskel through its type system can be obtain also in languages like C++, Swift and others. Uh, no. Sorry, that's just flatly wrong. Yes, static analysis tools are awesome, but you will never get the same level of compile-time safety from C++ that you will from Haskell or Rust or any number of functional languages. The type systems offer very little information, making it impossible for the compiler to shield anything.

blub 8y ago
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.
- tombert 8y ago
  I don’t know anything about SPARK or FramaC, but TLA+ isn’t a programming language, and you can use it to model distributed functional apps just fine (I still do). Even if the Erlang/Ericsson stuff is the “only case” (It’s not) I do not see how that makes my point less valid; Erlang was specifically design for systems that cannot fail. Telephones are just a good example of that.
  - blub 8y ago
    And doesn't your TLA+ model make your functional code significantly more reliable? Guess what, it does the same thing for OO languages => no need to use FP to increase reliability. Same goes for the other tools or languages I mentioned.