6 ms·

The software in the case of the 737 max performed exactly according to the spec. The problem is that the spec was buggy. The language can't fix a buggy spec. N

The software in the case of the 737 max performed exactly according to the spec. The problem is that the spec was buggy. The language can't fix a buggy spec. Note that the bug which caused the Ariane V disaster was written in Ada. And that was caused by the language. If the Ariane V code was written in C and the value simply overflowed, nothing negative would have happened. (The value would be hilariously wrong, but that wouldn't have mattered because the code wasn't necessary during flight. It was an oversight that it was running at all.) However, this is Ada, so it caused an integer overflow exception. Which was uncaught. Which caused the entire system to nope out. Which caused the rocket to blow up. So there's that to consider.

ajxs 7y ago
> "If the Ariane V code was written in C and the value simply overflowed, nothing negative would have happened" So... what you're saying is that the language not recognising an exception conditional has occurred is a better outcome in mission critical applications? "wasn't necessary", "It was an oversight", "Which was uncaught"... With these phrases you've already pointed out that the developers had improperly implemented the application.
- admax88q 7y ago
  There is something to be said for not just halting on an error in production systems. Its the same reason assertions are usually turned off on production builds. Yes ideally the programmers should have handled the exception, but once your in production and the system is running, should you really just halt the whole program due to an exception the prograera didn't foresee?
  - vore 7y ago
    For mission-critical software like avionics or a nuclear power plant? Absolutely! At design time you better figure out what all the error cases are, and blindly steamrolling over them when they should be triggered makes a bad problem worse (e.g. look at Cloudbleed where unchecked out-of-bounds reads starts disclosing other people's banking information). Assertions are also usually turned off for performance reasons, not to allow the program to plow through invariants being violated.
    - harry8 7y ago
      Uncaught exception and die. For a banking application, yes, die, hard, as loudly as possible. Downtime is worth it. Do not continue, do nothing until it is understood and fixed. When you're flying. Hmmm. Not so much. Dying is a really bad idea. Ok you should have it tested thoroughly so it isn't going to happen but if it does and "anything could happen" well "anything" is better than killing all the passengers, crew and anyone you might crash on, right? Literally anything is better than that. Idealy, you log it, you refuse to take off again, all the fleet is grounded etc etc but deciding to fall out of the sky because something unexpected happened is probably not the right response. Is graceful shutdown possible? No? Ok, so take your chances and log noisily is a less bad option.
      - MayeulC 7y ago
        Well, for an unmanned rocket, have it automatically self-destruct is likely the saner choice, as you don't want it to fall back somewhere inhabited, and there is usually little use for something on the wrong orbit.
      - Mikhail_Edoshin 7y ago
        The default out-of-box runtime can only handle one general scenario. The runtime designers choose to print the error message and terminate, and this seems to be the only sound option for default behavior. It's up to the developer to replace this default handler when the scenario differs that much.
        mumblemumble 7y ago
        > this seems to be the only sound option for default behavior I think that is the crux of this debate. In my background, yeah, you fail hard when anything unexpected happens. It's the most straightforward way to fail safe. But my background maps better to the financial case; I've never worked on avionics or anything like that. I can see the point, though, that, in that kind of situation, failing hard doesn't fail safe at all. It's conceivable to me that different problem domains require different default behavior. (And perhaps, by extension, different programming languages.)
  - nurettin 7y ago
    No, the process manager should log the stack trace, restart the subsystem and try running a few more times, then try an auxiliary system or just fly without the subsystem. It should not halt the whole software.
    - testrun 7y ago
      On a rocket launch?
      - nurettin 7y ago
        On projects which require redundancy and resilience.
  - feanaro 7y ago
    Ideally your type system should be aware of all the exceptions a particular function is able to throw so the compiler forces you to handle all of them before it compiles.
    - Mikhail_Edoshin 7y ago
      This is hardly possible. The whole idea of exceptions is that each function only deals with a subset. If no one does this, there's always a top-level handler that handles all. The default handler normally terminates the program, but it's totally possible to write a custom top-level handler that does something else. E.g. normally "out of memory" is an exception that causes a program to terminate, but in old Adobe Photoshop it was a routine situation that simply prompted the user to free some memory (by dropping the Undo, for example). I agree that the concept of the top-level handler and customization should be more visibly documented.
      - ernst_klim 7y ago
        > This is hardly possible. The whole idea of exceptions is that each function only deals with a subset. Why? It's totally possible to infer the most general type for all the functions in the program, hence to infer the type of the needed handler. Any language with subtyping and powerful type inference can do this, here is the toy ocaml example with typed algebraic effects (you can think of them as of exceptions): val read_file : path -[ Not_found ]-> string val process_content : string -[ OOM | Intern_err of int ]-> float let computation path = let content = read_file path in let result = process_content content in if result < 0 then raise Bad_result else result the type of computation would be inferred as val computation : path -[ Not_found | OOM | Intern_err of int | Bad_result ]-> float The handler should catch the corresponding exceptions. This could also be used with the result monad as well [1]. Even if you want to keep some exceptions unhandled, you can easily choose which ones, and track them carefully. [1] https://keleshev.com/composable-error-handling-in-ocaml https://keleshev.com/composable-error-handling-in-ocaml
        Mikhail_Edoshin 7y ago
  - rstuart4133 7y ago
    As a counter point, the Toyota ECU in those Camry's occasionally accelerated uncontrollably had asserts and what not. When they fired the system rebooted. From memory it took about a second to boot, so usually the driver didn't notice. Apparently it did that on a regular basis as it was overloaded, and sometimes it failed to meet deadlines. The acceleration problem was caused by noise flipping bits in the RAM the operating systems used to store state data. (The Toyota code was most immune to this because they duplicated their state by storing it in two different places, always compared on read and if it was different rebooted. But the OS was provided the the chip manufacturer, NEC which was a black box to Toyota - and it wasn't as conservative.) On rare occasions a bit flip would take out the watch dog process and the cruise control just after it decided to accelerate, and occasionally if that happened everyone in the vehicle died. Toyota blamed the deaths all sorts of things for a while - the driver, the carpet, third party accelerator pedals. Which to my mind was fair enough. They like everybody else had no idea what was causing it, but they knew their monitor / reboot if out of spec kludge worked very well so it was unlikely to be the ECU.
- alxlaz 7y ago
  What they are saying is that every language runtime, even stricter ones, has its own safety implications and you have to consider them when writing the specs and the code. Simply switching to a language with a stricter runtime may automagically take care of some simple cases, but no system is devoid of failure modes. Overflows are classic sources of disastrous bugs (e.g. the infamous THERAC-25). Switching to a system that detects them and raises an exception is a step in the right direction, but you still have to handle the exception cases correctly. And in some cases (like the Ariane V), incorrectly handling an exceptional condition turns out to be worse than allowing it to happen.
- w8rbt 7y ago
  C would recognize it, but not over-react. Log it and continue rather than going full abort/self destruct which is what ada did.
choonway 7y ago
The issue with Ariane V was the lack of integrated testing. If they had coupled the testing of the software with increased acceleration levels generated by a simulated Ariane V instead of an Ariane IV, they would have caught the issue. But let's say this was something unexpected - then probably the only way to mitigate this would be a backup system - but this is an unmanned system - and Apollo/Saturn/Shuttle/Soyuz levels of redundancies is not required.
- heisenbit 7y ago
  Yeah requirements were woefully incomplete, testing insufficient and may I add design where one unreliable sensor was wired to one processor which was given great authority over a system to wind in one direction very fast and where manual reversing out of was very slow or impossible when speeds got high (improbable when pitch directs you down). How could anyone believe this system was safe? No testing or requirements needed.
sterlind 7y ago
You can and should check your specs like they're code. For instance, you can write the spec in TLA+, which lets you specify temporal properties (e.g. "can the stall recovery procedure take an unbounded amount of time?") and liveness properties (e.g. "can any non-majority of disagreeing sensors cause the wrong trim actuations?") To test your invariants, you should sabotage the spec and check that invariants break. Once your spec passes model checking (or perhaps theorem proving with TLAPS), you can codify it in e.g. ADA-SPARK contracts. Once you have that, you've validated your spec, your contracts and your code. Bugs can only occur in your invariants and the seams of your subsystem. This level of rigor should be standard by now for safety-critical systems.
carlmr 7y ago
>The software in the case of the 737 max performed exactly according to the spec. The problem is that the spec was buggy. The language can't fix a buggy spec. That is true, but I found that in more strict languages you have a bit of a slower ramp-up, but the time you save later before production in bugs you don't have could be used to take more looks at the spec and better simulations. >If the Ariane V code was written in C and the value simply overflowed, nothing negative would have happened. In this particular case yes, however if the system was actually needed for flight (which I would guess most software is), it might be better to reset and retry. On average if your language fails hard like ADA it's also more likely to find these bugs in simulations and tests. Rust might have solved the problem the way you like it. Integer overflow causes exceptions only in Debug mode, not in Release mode.
- alxlaz 7y ago
  > That is true, but I found that in more strict languages you have a bit of a slower ramp-up, but the time you save later before production in bugs you don't have could be used to take more looks at the spec and better simulations. In many of these large companies in avionics (and not just avionics), the people writing the specs are not the same as the people writing the code. There is no trade-off between how much time it takes to write the code and how much time it takes to draft and review the specs. Edit: > On average if your language fails hard like ADA it's also more likely to find these bugs in simulations and tests. That is definitely ture, but it's important to keep two things in mind: 1. The possibility of a hard failure from your runtime is something that you need to be aware of at design time. As seen in the case that the parent comment mentioned, there are cases when a hard failure on a non-critical error is actually worse than allowing the error to occur. 2. More important, if it's hard failures that expose bugs during tests, the first thing you have to fix, even before you fix the code, is the test cases themselves. A hard failure during testing is an indication that the test cases you have don't cover a given situation and, more importantly, that your system can't even handle that situation. There are always going to be error conditions you can't recover from, and if they're in critical systems, you work around that (e.g. through redundancy). But a runtime that gives you a hard failure is rarely useful by itself.
ernst_klim 7y ago
> value simply overflowed, nothing negative would have happened. Except overflow would most likely have caused a significantly more severe outcome than the uncaught exception. And there is a restriction in GNAT (No_Exception_Propagation) which forces you to deal with any exception immediately, and should be used in any critical software imho. https://docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gnathie_ug/about_this_guide.html https://docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gna...
- mkl 7y ago
  Significantly more severe than the rocket blowing up?
alexeiz 7y ago
> this is Ada, so it caused an integer overflow exception This is not a language issue, but a general engineering one. In any critical system that can cause an unexpected exception and failure, there should be sufficient redundancy, so that when the main system goes down, the failover system can take control.

ajxs 7y ago

> "If the Ariane V code was written in C and the value simply overflowed, nothing negative would have happened" So... what you're saying is that the language not recognising an exception conditional has occurred is a better outcome in mission critical applications? "wasn't necessary", "It was an oversight", "Which was uncaught"... With these phrases you've already pointed out that the developers had improperly implemented the application.

admax88q 7y ago
There is something to be said for not just halting on an error in production systems. Its the same reason assertions are usually turned off on production builds. Yes ideally the programmers should have handled the exception, but once your in production and the system is running, should you really just halt the whole program due to an exception the prograera didn't foresee?
- vore 7y ago
  For mission-critical software like avionics or a nuclear power plant? Absolutely! At design time you better figure out what all the error cases are, and blindly steamrolling over them when they should be triggered makes a bad problem worse (e.g. look at Cloudbleed where unchecked out-of-bounds reads starts disclosing other people's banking information). Assertions are also usually turned off for performance reasons, not to allow the program to plow through invariants being violated.
  - harry8 7y ago
    Uncaught exception and die. For a banking application, yes, die, hard, as loudly as possible. Downtime is worth it. Do not continue, do nothing until it is understood and fixed. When you're flying. Hmmm. Not so much. Dying is a really bad idea. Ok you should have it tested thoroughly so it isn't going to happen but if it does and "anything could happen" well "anything" is better than killing all the passengers, crew and anyone you might crash on, right? Literally anything is better than that. Idealy, you log it, you refuse to take off again, all the fleet is grounded etc etc but deciding to fall out of the sky because something unexpected happened is probably not the right response. Is graceful shutdown possible? No? Ok, so take your chances and log noisily is a less bad option.
    - MayeulC 7y ago
      Well, for an unmanned rocket, have it automatically self-destruct is likely the saner choice, as you don't want it to fall back somewhere inhabited, and there is usually little use for something on the wrong orbit.
    - Mikhail_Edoshin 7y ago
      The default out-of-box runtime can only handle one general scenario. The runtime designers choose to print the error message and terminate, and this seems to be the only sound option for default behavior. It's up to the developer to replace this default handler when the scenario differs that much.
      - mumblemumble 7y ago
        > this seems to be the only sound option for default behavior I think that is the crux of this debate. In my background, yeah, you fail hard when anything unexpected happens. It's the most straightforward way to fail safe. But my background maps better to the financial case; I've never worked on avionics or anything like that. I can see the point, though, that, in that kind of situation, failing hard doesn't fail safe at all. It's conceivable to me that different problem domains require different default behavior. (And perhaps, by extension, different programming languages.)
- nurettin 7y ago
  No, the process manager should log the stack trace, restart the subsystem and try running a few more times, then try an auxiliary system or just fly without the subsystem. It should not halt the whole software.
  - testrun 7y ago
    On a rocket launch?
    - nurettin 7y ago
      On projects which require redundancy and resilience.
- feanaro 7y ago
  Ideally your type system should be aware of all the exceptions a particular function is able to throw so the compiler forces you to handle all of them before it compiles.
  - Mikhail_Edoshin 7y ago
    This is hardly possible. The whole idea of exceptions is that each function only deals with a subset. If no one does this, there's always a top-level handler that handles all. The default handler normally terminates the program, but it's totally possible to write a custom top-level handler that does something else. E.g. normally "out of memory" is an exception that causes a program to terminate, but in old Adobe Photoshop it was a routine situation that simply prompted the user to free some memory (by dropping the Undo, for example). I agree that the concept of the top-level handler and customization should be more visibly documented.
    - ernst_klim 7y ago
      > This is hardly possible. The whole idea of exceptions is that each function only deals with a subset. Why? It's totally possible to infer the most general type for all the functions in the program, hence to infer the type of the needed handler. Any language with subtyping and powerful type inference can do this, here is the toy ocaml example with typed algebraic effects (you can think of them as of exceptions): val read_file : path -[ Not_found ]-> string val process_content : string -[ OOM | Intern_err of int ]-> float let computation path = let content = read_file path in let result = process_content content in if result < 0 then raise Bad_result else result the type of computation would be inferred as val computation : path -[ Not_found | OOM | Intern_err of int | Bad_result ]-> float The handler should catch the corresponding exceptions. This could also be used with the result monad as well [1]. Even if you want to keep some exceptions unhandled, you can easily choose which ones, and track them carefully. [1] https://keleshev.com/composable-error-handling-in-ocaml https://keleshev.com/composable-error-handling-in-ocaml
      - Mikhail_Edoshin 7y ago
- rstuart4133 7y ago
  As a counter point, the Toyota ECU in those Camry's occasionally accelerated uncontrollably had asserts and what not. When they fired the system rebooted. From memory it took about a second to boot, so usually the driver didn't notice. Apparently it did that on a regular basis as it was overloaded, and sometimes it failed to meet deadlines. The acceleration problem was caused by noise flipping bits in the RAM the operating systems used to store state data. (The Toyota code was most immune to this because they duplicated their state by storing it in two different places, always compared on read and if it was different rebooted. But the OS was provided the the chip manufacturer, NEC which was a black box to Toyota - and it wasn't as conservative.) On rare occasions a bit flip would take out the watch dog process and the cruise control just after it decided to accelerate, and occasionally if that happened everyone in the vehicle died. Toyota blamed the deaths all sorts of things for a while - the driver, the carpet, third party accelerator pedals. Which to my mind was fair enough. They like everybody else had no idea what was causing it, but they knew their monitor / reboot if out of spec kludge worked very well so it was unlikely to be the ECU.
alxlaz 7y ago
What they are saying is that every language runtime, even stricter ones, has its own safety implications and you have to consider them when writing the specs and the code. Simply switching to a language with a stricter runtime may automagically take care of some simple cases, but no system is devoid of failure modes. Overflows are classic sources of disastrous bugs (e.g. the infamous THERAC-25). Switching to a system that detects them and raises an exception is a step in the right direction, but you still have to handle the exception cases correctly. And in some cases (like the Ariane V), incorrectly handling an exceptional condition turns out to be worse than allowing it to happen.
w8rbt 7y ago
C would recognize it, but not over-react. Log it and continue rather than going full abort/self destruct which is what ada did.

choonway 7y ago

The issue with Ariane V was the lack of integrated testing. If they had coupled the testing of the software with increased acceleration levels generated by a simulated Ariane V instead of an Ariane IV, they would have caught the issue. But let's say this was something unexpected - then probably the only way to mitigate this would be a backup system - but this is an unmanned system - and Apollo/Saturn/Shuttle/Soyuz levels of redundancies is not required.

heisenbit 7y ago
Yeah requirements were woefully incomplete, testing insufficient and may I add design where one unreliable sensor was wired to one processor which was given great authority over a system to wind in one direction very fast and where manual reversing out of was very slow or impossible when speeds got high (improbable when pitch directs you down). How could anyone believe this system was safe? No testing or requirements needed.

sterlind 7y ago

You can and should check your specs like they're code. For instance, you can write the spec in TLA+, which lets you specify temporal properties (e.g. "can the stall recovery procedure take an unbounded amount of time?") and liveness properties (e.g. "can any non-majority of disagreeing sensors cause the wrong trim actuations?") To test your invariants, you should sabotage the spec and check that invariants break. Once your spec passes model checking (or perhaps theorem proving with TLAPS), you can codify it in e.g. ADA-SPARK contracts. Once you have that, you've validated your spec, your contracts and your code. Bugs can only occur in your invariants and the seams of your subsystem. This level of rigor should be standard by now for safety-critical systems.

carlmr 7y ago

>The software in the case of the 737 max performed exactly according to the spec. The problem is that the spec was buggy. The language can't fix a buggy spec. That is true, but I found that in more strict languages you have a bit of a slower ramp-up, but the time you save later before production in bugs you don't have could be used to take more looks at the spec and better simulations. >If the Ariane V code was written in C and the value simply overflowed, nothing negative would have happened. In this particular case yes, however if the system was actually needed for flight (which I would guess most software is), it might be better to reset and retry. On average if your language fails hard like ADA it's also more likely to find these bugs in simulations and tests. Rust might have solved the problem the way you like it. Integer overflow causes exceptions only in Debug mode, not in Release mode.

alxlaz 7y ago
> That is true, but I found that in more strict languages you have a bit of a slower ramp-up, but the time you save later before production in bugs you don't have could be used to take more looks at the spec and better simulations. In many of these large companies in avionics (and not just avionics), the people writing the specs are not the same as the people writing the code. There is no trade-off between how much time it takes to write the code and how much time it takes to draft and review the specs. Edit: > On average if your language fails hard like ADA it's also more likely to find these bugs in simulations and tests. That is definitely ture, but it's important to keep two things in mind: 1. The possibility of a hard failure from your runtime is something that you need to be aware of at design time. As seen in the case that the parent comment mentioned, there are cases when a hard failure on a non-critical error is actually worse than allowing the error to occur. 2. More important, if it's hard failures that expose bugs during tests, the first thing you have to fix, even before you fix the code, is the test cases themselves. A hard failure during testing is an indication that the test cases you have don't cover a given situation and, more importantly, that your system can't even handle that situation. There are always going to be error conditions you can't recover from, and if they're in critical systems, you work around that (e.g. through redundancy). But a runtime that gives you a hard failure is rarely useful by itself.

ernst_klim 7y ago

> value simply overflowed, nothing negative would have happened. Except overflow would most likely have caused a significantly more severe outcome than the uncaught exception. And there is a restriction in GNAT (No_Exception_Propagation) which forces you to deal with any exception immediately, and should be used in any critical software imho. https://docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gnathie_ug/about_this_guide.html https://docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gna...

mkl 7y ago
Significantly more severe than the rocket blowing up?

alexeiz 7y ago

> this is Ada, so it caused an integer overflow exception This is not a language issue, but a general engineering one. In any critical system that can cause an unexpected exception and failure, there should be sufficient redundancy, so that when the main system goes down, the failover system can take control.