[taeric]

What the shit? Your question: "You are given two systems, one implemented in language class X, one implemented in language class Y, pick the one you trust." Me: "Not enough information to make a valid answer."

To be clear, I think mistakes have been made with all paradigms of programming. In many cases, the mistakes were made completely outside the realm of the program. Like the Ariane example. I only mentioned it as a "failure" of static typing because of your bloody question.

Seriously, it is your hypothetical: "Here is a rocket where the control system was implemented in Ada. Do you trust it more than a competing one that was implemented in machine language?" That is essentially the question you gave me. I turned it around precisely to show that just knowing the type of language that something was implemented in is bloody worthless.

I have made up my mind. To remain skeptical of claims that are not backed by empirical evidence. I'm optimistic enough to think that static typing is actually a good thing. The arguments used to put it lack any backing with verification. (Which, I find ironic, since they are supposed to be about verification.)

[srean]

Ah I see what happened. We somehow managed to talk past each other and go out of sync and ended up responding to something that was not on the others mind.

If you thought I am not in agreement with this comment of yours, then let me assure you that I am (with certain differences).

My point remains that your Ariane example is irrelevant, it shows that statically typed systems can still fail if there are failure modes outside of the purview of the typechecker. That is obvious and was never in contest. What was in contest, however, was the relative safeties of statically typed vs dynamically typed. Your example has no bearing in clearing that question. I am claiming superiority of the static paradigm because no one has been forthcoming in putting their money and lives in control of a dynamically typed controller. You are just refusing to concede this because it affects your view in some way, and I dont expect to see any change in that behavior.

Let me put forward my main claim (and ignore the silly hypothetical ones): dynamically typed/checked languages are unsuitable and dangerous for cases where runtime errors are egregiously costly because they cannot prove that such eventualities cannot happen before they actually happen. Because of these risks involved such systems are sensibly not implemented in dynamically typed/checked languages. Statically typed languages cannot immunizes against all possible failures, yet they are better than dynamically typed languages in this scenario because they can eliminate a large class of these runtime errors that dynamically typed languages just cannot (if they can they are statically typed by definition), whereas testing applies equally to both.

BTW a dynamically typed language with exhaustive static analysis is a statically typechecked language.

[taeric]

Makes sense. Though, I disagree with your last assertion. That is, no matter how exhaustively a solution has been explored, if the implementation language is a dynamic one, then it is implemented in a dynamic language.

As an example, I take any of the MIX algorithms in Knuth's books. They are more thoroughly documented and explained than anything under other software I have ever seen. They still aren't statically typed. (Simply put, if someone makes a mistake in transcribing it or "cleaning" it up, it will not be caught by a type checker.)

And, yes, I do think we ultimately agree. The heart of my question is just wanting evidence. I even agree with the premise that "in the absence of other evidence*, I would have more faith in a statically typed solution than otherwise. I just wouldn't have that much faith without more. :)