31 ms·

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 practice

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.
- JabavuAdams 6y ago
  Agree with most of what you've written -- thanks for the thoughtful response. Was going to respond that I recall the F-35 uses C++, but that's probably not a good argument ... Regarding choice of language, I've reached a level of general competence where I don't really find any intractable problems that I can't handle with my toolset. So part of this may be just personal preference where there's no justification for slogging through the cost of learning yet another language, especially if I don't find it fun to program in. I used to invest a lot of time in learning new languages but I no longer find this a good use of my time. I own a handful of Haskell books, and I was originally interested in Haskell for abstraction / DSLs. One idea was to go directly from a human-readable binary file-format description to an importer/exporter for that file type. Questions on a couple of themes: 1) I have gone back to uni to study biophysics and learning biology deeply as well as previous machine-learning experience is making me think that fuzzy / probabilistic / redundant is actually the way to go for reliable complex systems. What we consider to be complex computer systems are actually ridiculously simple compared to biological mechanisms. 2) Are we in a transitional phase such that inventing better programming languages is an inefficient (though of course interesting and possibly instructive) path? Do we get machine-programmers soon enough that programming-language design stops mattering? By analogy think of all the effort still being spent on machine-readable data formats when we're close to having machines that read. At that point anything human-readable becomes machine-readable and your schema doesn't really matter.
  - tome 6y ago
    Just to clarify, when Haskellers say that Haskell is good for "correctness" they don't mean it is good for "verification"[1]. "Verification" means something like "formally proving the behaviour of a system". It is very hard. "Correctness" to Haskellers means modest things like "the compiler tells me when I passed a NULL (Nothing) to a function that didn't expect it" or "the compiler tells me when I mixed a part name for a part serial number". Modest, but nonetheless Haskell does this in a ergonomic way which is very effective for writing quality software. [1] or at least any reasonable ones don't
  - ghc 6y ago

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.

JabavuAdams 6y ago
Agree with most of what you've written -- thanks for the thoughtful response. Was going to respond that I recall the F-35 uses C++, but that's probably not a good argument ... Regarding choice of language, I've reached a level of general competence where I don't really find any intractable problems that I can't handle with my toolset. So part of this may be just personal preference where there's no justification for slogging through the cost of learning yet another language, especially if I don't find it fun to program in. I used to invest a lot of time in learning new languages but I no longer find this a good use of my time. I own a handful of Haskell books, and I was originally interested in Haskell for abstraction / DSLs. One idea was to go directly from a human-readable binary file-format description to an importer/exporter for that file type. Questions on a couple of themes: 1) I have gone back to uni to study biophysics and learning biology deeply as well as previous machine-learning experience is making me think that fuzzy / probabilistic / redundant is actually the way to go for reliable complex systems. What we consider to be complex computer systems are actually ridiculously simple compared to biological mechanisms. 2) Are we in a transitional phase such that inventing better programming languages is an inefficient (though of course interesting and possibly instructive) path? Do we get machine-programmers soon enough that programming-language design stops mattering? By analogy think of all the effort still being spent on machine-readable data formats when we're close to having machines that read. At that point anything human-readable becomes machine-readable and your schema doesn't really matter.
- tome 6y ago
  Just to clarify, when Haskellers say that Haskell is good for "correctness" they don't mean it is good for "verification"[1]. "Verification" means something like "formally proving the behaviour of a system". It is very hard. "Correctness" to Haskellers means modest things like "the compiler tells me when I passed a NULL (Nothing) to a function that didn't expect it" or "the compiler tells me when I mixed a part name for a part serial number". Modest, but nonetheless Haskell does this in a ergonomic way which is very effective for writing quality software. [1] or at least any reasonable ones don't
- ghc 6y ago