4 ms·

Haskell is good for correctness. Where correctness really matters, you might find Haskell. That makes it a very niche language, as most developers don't really

by ghc 6y ago

Haskell is good for correctness. Where correctness really matters, you might find Haskell. That makes it a very niche language, as most developers don't really care about correctness. But you do find Haskell in places where complexity is high and correctness matters. Mostly banking, infrastructure, defense, and research applications.

newswasboring 6y ago
Everyone makes this point about correctness, but I have never seen an easy to understand illustration of this. Now I am by no means a leet programmer but I have been reading about programming for more than a decade and every article about this point feels confusing. I even tried writing small stuff in haskell, still don't get this point.
- alisonkisk 6y ago
  Correctness is only an interesting problem when it's not easy to underst example and. Easy bloggable examples aren't complex enough to be correctness challenges
  - newswasboring 6y ago
    Ok. Then what book can I read to understand this. I've read two books on haskell but they were beginner stuff though
    - ghc 6y ago
      Closest I can think of is Purely Functional Data Structure (Chris Okasaki) or Category Theory for Programmers (Bartosz Milewski), but they're not exactly what you're after. I would submit that this paper from FB is more in the vein of what you're looking for: https://research.fb.com/wp-content/uploads/2020/08/Eliminating-Bugs-with-Dependent-Haskell-Experience-Report.pdf https://research.fb.com/wp-content/uploads/2020/08/Eliminati... . This interview might also be insightful: https://www.microsoft.com/en-us/research/podcast/functional-programming-languages-pursuit-laziness-dr-simon-peyton-jones/ https://www.microsoft.com/en-us/research/podcast/functional-... The truth is that Haskell is still very academically focused, so you're likely to see papers of substance much more often than books or blog posts. When you hire people to write Haskell there's two groups that always show up: young enthusiasts who are frustrated with imperative programming in their (usually first or second) day job, and academics who got transplanted into industry to work on hard problems. I've interviewed people doing formal verification of CPU circuits at Intel, people who work on compilers, people who work on verifying termination of programs (for missile guidance), and people who work on financial institution backends. What I haven't seen is too many experienced, pragmatic engineers (rather than computer scientists) who have spent their career writing Haskell.
JabavuAdams 6y ago
The thing is correctness should not be viewed as the role of the language alone. You have to look at the whole ecosystem and organizational engineering practices. Obviously people were writing life-critical code in C or ASM. You wouldn't expect a car manufacturer to write an ECU in the same way a game dev studio writes a game, but C and ASM can accommodate both. From my experience Haskell seems to make easy things hard. It's the same mistake as a small startup thinking they need to do whatever Google / Facebook / Amazon are doing, when they're operating at one millionth the scale. EDIT> By not focusing on correctness as the role of the language alone, you have a smooth path from quickly iterating in a non-safety-critical environment to whatever level of safety you need. In engineering safety is empirical, anyway. You don't just build a system and then assume it will work absent tests, so the idea of getting the code perfect is a bit of a red herring. You're going to have to test it rigorously anyway before anyone will get on your airplane.
- deleted 6y ago
  [deleted]
- ghc 6y ago
  There's a large body of academic research on this, and many, many failures to learn from, including many that cost lives or cost hundreds of millions of dollars. In practice, there are lots and lots of bugs in any C program of any complexity. That's why flight system software is written in Ada, not C. In the military where you need to verify correctness of security controls or answer questions like "does my missile guidance program terminate", you can't use C or Assembly. To achieve what you're talking about with C or Assembly, you need this kind of process: https://www.fastcompany.com/28121/they-write-right-stuff https://www.fastcompany.com/28121/they-write-right-stuff To achieve it with a dynamic language like Python...well, you can't (and shouldn't even attempt it). The trouble is, nobody has the budget for that. Not even most military groups. So instead of relying on human process, we leverage machine-driven verification through the use of type systems, provers, SAT solvers, contracts, randomized testing and other academically sound techniques for quality assurance. > From my experience Haskell seems to make easy things hard. Haskell isn't designed to make undergraduate programming exercises easy. It's designed to make hard programming problems tractable. If you have an easy problem you shouldn't use Haskell. Hell, if you have a hard problem you probably shouldn't use Haskell.

by ghc 6y ago

newswasboring 6y ago

Everyone makes this point about correctness, but I have never seen an easy to understand illustration of this. Now I am by no means a leet programmer but I have been reading about programming for more than a decade and every article about this point feels confusing. I even tried writing small stuff in haskell, still don't get this point.

alisonkisk 6y ago
Correctness is only an interesting problem when it's not easy to underst example and. Easy bloggable examples aren't complex enough to be correctness challenges
- newswasboring 6y ago
  Ok. Then what book can I read to understand this. I've read two books on haskell but they were beginner stuff though
  - ghc 6y ago
    Closest I can think of is Purely Functional Data Structure (Chris Okasaki) or Category Theory for Programmers (Bartosz Milewski), but they're not exactly what you're after. I would submit that this paper from FB is more in the vein of what you're looking for: https://research.fb.com/wp-content/uploads/2020/08/Eliminating-Bugs-with-Dependent-Haskell-Experience-Report.pdf https://research.fb.com/wp-content/uploads/2020/08/Eliminati... . This interview might also be insightful: https://www.microsoft.com/en-us/research/podcast/functional-programming-languages-pursuit-laziness-dr-simon-peyton-jones/ https://www.microsoft.com/en-us/research/podcast/functional-... The truth is that Haskell is still very academically focused, so you're likely to see papers of substance much more often than books or blog posts. When you hire people to write Haskell there's two groups that always show up: young enthusiasts who are frustrated with imperative programming in their (usually first or second) day job, and academics who got transplanted into industry to work on hard problems. I've interviewed people doing formal verification of CPU circuits at Intel, people who work on compilers, people who work on verifying termination of programs (for missile guidance), and people who work on financial institution backends. What I haven't seen is too many experienced, pragmatic engineers (rather than computer scientists) who have spent their career writing Haskell.

JabavuAdams 6y ago

The thing is correctness should not be viewed as the role of the language alone. You have to look at the whole ecosystem and organizational engineering practices. Obviously people were writing life-critical code in C or ASM. You wouldn't expect a car manufacturer to write an ECU in the same way a game dev studio writes a game, but C and ASM can accommodate both. From my experience Haskell seems to make easy things hard. It's the same mistake as a small startup thinking they need to do whatever Google / Facebook / Amazon are doing, when they're operating at one millionth the scale. EDIT> By not focusing on correctness as the role of the language alone, you have a smooth path from quickly iterating in a non-safety-critical environment to whatever level of safety you need. In engineering safety is empirical, anyway. You don't just build a system and then assume it will work absent tests, so the idea of getting the code perfect is a bit of a red herring. You're going to have to test it rigorously anyway before anyone will get on your airplane.

deleted 6y ago
[deleted]
ghc 6y ago
There's a large body of academic research on this, and many, many failures to learn from, including many that cost lives or cost hundreds of millions of dollars. In practice, there are lots and lots of bugs in any C program of any complexity. That's why flight system software is written in Ada, not C. In the military where you need to verify correctness of security controls or answer questions like "does my missile guidance program terminate", you can't use C or Assembly. To achieve what you're talking about with C or Assembly, you need this kind of process: https://www.fastcompany.com/28121/they-write-right-stuff https://www.fastcompany.com/28121/they-write-right-stuff To achieve it with a dynamic language like Python...well, you can't (and shouldn't even attempt it). The trouble is, nobody has the budget for that. Not even most military groups. So instead of relying on human process, we leverage machine-driven verification through the use of type systems, provers, SAT solvers, contracts, randomized testing and other academically sound techniques for quality assurance. > From my experience Haskell seems to make easy things hard. Haskell isn't designed to make undergraduate programming exercises easy. It's designed to make hard programming problems tractable. If you have an easy problem you shouldn't use Haskell. Hell, if you have a hard problem you probably shouldn't use Haskell.