Yes, runtime faults can happen in a static language as well.
However, I don't buy the usual argument that follows up (not saying you are saying this now, but I'm sure you've heard it): "therefore, you're not better off using a statically typed language, therefore just use a dynamically typed language".
Just because a statically typed language cannot rule out every kind of runtime flaw is not a good reason to stop using them. Statically typed languages rule out some errors that dynamically typed languages don't. In both cases you also need to perform additional checks, and in both cases, safety critical systems should be formally verified. Not "instead", but "in addition to".
A statically typed language is an additional, automatic safety net on top of everything else. Every bit of safety counts. You don't need to formally verify your generic list algorithm isn't going to try adding two elements (and throw an exception when the elements cannot be meaningfully added) because it can't by definition. That's one less formal verification you need to do.
I never claimed dynamic languages were better, just that Haskell is a dynamic language with more static features than say Python. There are no truly static languages, except maybe perhaps static macro languages like C++'s STL.
> In both cases you also need to perform additional checks, and in both cases, safety critical systems should be formally verified. Not "instead", but "in addition to".
In practice, there are a lot of other things going on in Haskell that work against formal verification in safety critical real time systems. When you need to know for sure, non-determinism (say in the form of lazy evaluation) is your enemy, and the type system itself becomes less useful because those paths have to be rigorously explored anyhow. Heck, at that point, you might even want to use assembly since even the compiler is suspect.
Thankfully, most of us don't write that kind of code.
Pedantic: runtime is a thing that runs your program while run-time is a phase.
> I never claimed dynamic languages were better, just that Haskell is a dynamic language with more static features than say Python. There are no truly static languages, except maybe perhaps static macro languages like C++'s STL.
That's a pretty non-standard view. It's as unhelpful as static typing proponents claiming dynamically typed languages such as Python are "unityped". As unhelpful as Simon Peyton Jones jokingly claiming that Haskell is the world's best imperative language :) Any of those claims may be technically true, but it doesn't help us understand, choose or use those languages. Other similarly unhelpful claims include the old "these languages are all Turing-complete anyway, so it doesn't which one you use."
So I disagree with you, philosophically, but since I acknowledge you're a very knowledgeable guy, let me ask you about your opinion:
- Would you say there is no advantage to using a statically typed language like Haskell/ML over a dynamically typed language?
- Or if you think there is an advantage, do you think the costs outweigh the benefits?
- If you were asked to develop a safety critical system, and given the choice of using Haskell (or ML if you dislike lazy evaluation by default, or OCaml if you prefer a more hybrid language) and Python (or a similar dynamic language of your choice), and every other analysis tool you can think of, static or run-time, which language would you pick? Assume you cannot pick anything else, you're given time to become proficient on the language you pick, and you cannot refuse the assignment. I know, this is a fantasy scenario, but indulge me.
Static typing is definitely useful, but like humans and chimps, the so called static languages share much of their DNA with their dynamic counterparts; and static typing doesn't necessarily account for more than a few percentage points of productivity increases (though those percents are definitely noticeable). More to the point, you still need to test non trivial Haskell code and the lack of a decent debugger is a tragedy.
Safety critical systems are generally real tine so Haskell is off the table. I'll also spend a lot of tine manually verifying the code, and using alot of external analysis and verification tools, so restricted C++ is fine in that case. Now, if you told me that the system was safety critical and nit real time, and the system wasn't important enough to merit lots of manual verification, then Haskell would be a great choice because its static type system is better than nothing.
Why do you think Haskell is fine as long as the system "isn't important enough to merit lots of manual verification"? That sounds puzzling to me. I'd say one thing complements the other: automatic and manual verification seems the best option.
Is lazy evaluation your biggest issue with Haskell? How about languages like ML or OCaml, which are arguably safer than "restricted C++" and do not default to lazy evaluation?
Or is GC your main problem with these languages? This would rule out most dynamically typed languages as well.
Most languages focus on productivity, because that is where the market it is. Safety critical systems are not dominated at all by productivity concerns, and a lot of resources are thrown at them to make sure they are perfect. In this case, the abstractions provided by any HLL just get in the way! Its like putting a cattle guard on front of a tank.
Anyways, you might want to read the stack overflow article on this subject:
However, I don't buy the usual argument that follows up (not saying you are saying this now, but I'm sure you've heard it): "therefore, you're not better off using a statically typed language, therefore just use a dynamically typed language".
Just because a statically typed language cannot rule out every kind of runtime flaw is not a good reason to stop using them. Statically typed languages rule out some errors that dynamically typed languages don't. In both cases you also need to perform additional checks, and in both cases, safety critical systems should be formally verified. Not "instead", but "in addition to".
A statically typed language is an additional, automatic safety net on top of everything else. Every bit of safety counts. You don't need to formally verify your generic list algorithm isn't going to try adding two elements (and throw an exception when the elements cannot be meaningfully added) because it can't by definition. That's one less formal verification you need to do.