3 ms·
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
by 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 agoAgree 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 agoJust 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> Was going to respond that I recall the F-35 uses C++ AFAIK its critical flight systems are still in Ada, but it's a beast of a software platform. My company joined the effort last year and found that even our tiny area was an incredible mess of different technologies. > 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. Personally I wouldn't learn new tools unless your existing toolset proved inadequate. But I'm pretty jaded at this point. Learning new techniques, on the other hand, I would never stop doing. Everything from design patterns to compiler design, from dynamic programming to category theory - it all has made me a better programmer regardless of the tools I have at my disposal. > !) & 2) I agree on 1, to a certain extent. The trouble with that approach is the development time of solutions is pretty excessive. Ironically probabilistic programming suffers from this same issue. I would be satisfied is software engineering was just actual engineering, which it isn't. I don't think we'll achieve the transition of software into an engineering discipline until we have better methods of communicating to both the human and computer in parallel. My guess is we might be 50 to 100 years away still.