3 ms·

> :( Why are we replying without going down the chain? I dislike deeply nested, indentation cramped and tangential threads, so sometimes if I dont have anythin

by srean 12y ago

> :( Why are we replying without going down the chain? I dislike deeply nested, indentation cramped and tangential threads, so sometimes if I dont have anything that important to say I inline it. More so when everyone has left the building. > I'm also familiar with some fun disasters using software by Ada. I dont think we were ever discussing whether using Ada or some other statically type checked language immunizes a project against all other peripheral errors. That would be a supremely ridiculous and stupid claim to make. Typechecking proves either that the code is type error free or that the typechecker has a bug. In the case of the latter, you try and fix it and the benefit percolates to every software verified by it. Testing proves that it passes only those specific test cases and only if the programmer tested it at all. BTW the very first line says the fault had nothing to do with Ada. The source of the error was beyond the scope of typechecking. To backtrack, our discussion was on whether there are notable examples of software written in dynamically typed languages where the cost of error is high. Runtime error while spaceshuttle descends backs to earth, no thank you, on a fly-by-wire unit, when the pilot is breaking out of a loop, again no thank you. There are times when, no pun intended, you just cannot bail out and wash your hands off the situation, without terrible consequences. In such cases I would rather have the error surfaced in an environment where I can control the consequences, meaning early, and as exhaustively as possible. Most importantly typechecking does not preclude/replace testing, it complements it. Everything cannot be statically verified or insured against, but that does not mean that just because we cannot verify everything statically, we should verify nothing statically. BTW Typical x-ray machines do not have the power to kill you in a single exposure, radiotherapy units absolutely can, example Therac. The accidents occurred when the high-power electron beam was activated instead of the intended low power beam, and without the beam spreader plate rotated into place. Previous models had hardware interlocks in place to prevent this, but Therac-25 had removed them, depending instead on software interlocks for safety. The software interlock could fail due to a race condition. I would rather have it proved (exhaustively, rather than with typical tests which would be anecdotaly) that such errors cannot happen.

taeric 12y ago
Well, apologies for the nesting. :( I agree it is ugly, but is easier to spot changes. (Also.... I went to sleep. Sorry. Which, also, I was tired. My tone has been terrible in some of these messages. Apologies for that, as well. To all involved.) I am aware, and agree with the opinion, that Ada had nothing to do with the error. However, I don't think many would disagree that the fact the code was in Ada gave the team that decided to reuse it more faith that it was "safely" reusable than had it been written in another language. This is still not the fault of Ada, but it was the exact reasoning you are using to say I should prefer the statically typed solution over another, if that is all I know. My point is if that is all you know, you don't know enough to make a decision. So, in my mind, our discussion was not over whether there are notable examples of software written in dynamically typed languages where the cost of error is high. The discussion is whether there have been studies showing that statically typed languages produce less bug prone software. So, to your own example, what was Therac written in? Because, honestly, right off I don't know. I would not be surprised to know it was in a statically typed language. And note, I would not use that as an example of where typed safe languages are failures. And then to wrap up back to your question. It doesn't take a lot of googling to find that Nasa used to use a Symbolics Lisp machine in their work. http://stackoverflow.com/a/563378/392812 http://stackoverflow.com/a/563378/392812
- srean 12y ago
  > that the fact the code was in Ada gave the team that decided to reuse it more faith that it was "safely" reusable than had it been written in another language. And you are making ridiculous analogies from the Ariane example. Ada had no bearing on the failure. They plugged in a controller for a different vehicle entirely. The question is about relative confidence between a statically typed and a runtime typed software. The fact remains that given a fixed/finite budget of testing, wise people will not even think of deploying a runtime typed system for such tasks. These tasks cannot afford runtime errors, so it is imperative that due diligence be made to prove that they cannot happen. (You cannot send several manned missions to the moon just to test) I am not aware of runtime typed systems that afford such proofs before running it and if some do, it is a statically proven system to begin with. Revisit my points about runtime errors on a flight controller. Or to be less fancy, runtime error in trading software, "oops sent the wrong million dollar transaction request and bailed out because of runtime error". Has happened, and run companies to the ground. > what was Therac written in? Given its age, I would assume it was some fairly low level language. Whatever it was, it was something that did not prove that such races cannot happen, in other words it was open to runtime error, which is exactly what we want to eliminate as far as possible. We will run it a few times and see what gives, is not a tenable strategy for many important tasks. > It doesn't take a lot of googling to find that Nasa used to use a Symbolics Lisp machine You are being slightly disingenuous here, I was talking about deployed flight controllers that actually control the thing when its on flight. As I have said its like arguing with birthers, you have made up your mind and no matter what I say you will try to avoid the logic of eliminating costly runtime errors.

by srean 12y ago

taeric 12y ago

Well, apologies for the nesting. :( I agree it is ugly, but is easier to spot changes. (Also.... I went to sleep. Sorry. Which, also, I was tired. My tone has been terrible in some of these messages. Apologies for that, as well. To all involved.) I am aware, and agree with the opinion, that Ada had nothing to do with the error. However, I don't think many would disagree that the fact the code was in Ada gave the team that decided to reuse it more faith that it was "safely" reusable than had it been written in another language. This is still not the fault of Ada, but it was the exact reasoning you are using to say I should prefer the statically typed solution over another, if that is all I know. My point is if that is all you know, you don't know enough to make a decision. So, in my mind, our discussion was not over whether there are notable examples of software written in dynamically typed languages where the cost of error is high. The discussion is whether there have been studies showing that statically typed languages produce less bug prone software. So, to your own example, what was Therac written in? Because, honestly, right off I don't know. I would not be surprised to know it was in a statically typed language. And note, I would not use that as an example of where typed safe languages are failures. And then to wrap up back to your question. It doesn't take a lot of googling to find that Nasa used to use a Symbolics Lisp machine in their work. http://stackoverflow.com/a/563378/392812 http://stackoverflow.com/a/563378/392812

srean 12y ago
> that the fact the code was in Ada gave the team that decided to reuse it more faith that it was "safely" reusable than had it been written in another language. And you are making ridiculous analogies from the Ariane example. Ada had no bearing on the failure. They plugged in a controller for a different vehicle entirely. The question is about relative confidence between a statically typed and a runtime typed software. The fact remains that given a fixed/finite budget of testing, wise people will not even think of deploying a runtime typed system for such tasks. These tasks cannot afford runtime errors, so it is imperative that due diligence be made to prove that they cannot happen. (You cannot send several manned missions to the moon just to test) I am not aware of runtime typed systems that afford such proofs before running it and if some do, it is a statically proven system to begin with. Revisit my points about runtime errors on a flight controller. Or to be less fancy, runtime error in trading software, "oops sent the wrong million dollar transaction request and bailed out because of runtime error". Has happened, and run companies to the ground. > what was Therac written in? Given its age, I would assume it was some fairly low level language. Whatever it was, it was something that did not prove that such races cannot happen, in other words it was open to runtime error, which is exactly what we want to eliminate as far as possible. We will run it a few times and see what gives, is not a tenable strategy for many important tasks. > It doesn't take a lot of googling to find that Nasa used to use a Symbolics Lisp machine You are being slightly disingenuous here, I was talking about deployed flight controllers that actually control the thing when its on flight. As I have said its like arguing with birthers, you have made up your mind and no matter what I say you will try to avoid the logic of eliminating costly runtime errors.