6 ms·

I'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one ne

by bollu 8y ago

I'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one needs to write to get anything done. For reference, the certified compiler CompCert's code base is something like 10% code and 90% proofs.

crimsonalucard 8y ago
No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.
- scrape_it 8y ago
  Well, to support the top parent's comment, here's what John Carmack had to say about SAAB's fighter jet: > The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling it what to do, but this worked out well for testing: all data was allocated statically, and monitoring those variables gave a clear picture of most everything the software was doing. The software did only the bare essentials, and of course, they were serious about thorough ground testing. > No bug has ever been found in the “released for flight” versions of that code. so not quite that tests are useless because blackbox, but more that yes, it is possible to write software that facilitates showing a code will do what it says it will do. In another note, I do feel sorry for the engineers but at the same time Airbus also has similar MCAS system, but the only thing that saves them is an extra Angle-of-Attack sensor whereas I believe the boeing relied on just one or two. Airbus had 3 AOA sensors and if 2 agreed, that was the data fed into the MCAS. It still boggles my mind that they would place a bigger engine when the original plane was not built for it at all, this was 100% profit orientated move to prevent Airbus from taking Boeing's majority marketshare, it's highly ironic that the opposite results. Even more infuriating is that Boeing passed it off as the exact same plane, not much extra training is necessary, along with FAA giving their blessing, now caught up in the mess. Canada for instance is now looking to the EU for an independent auditing, as any credibility FAA has built up over the past years has taken a significant hit.
  - mongol 8y ago
    Interesting quote. Seems it was actually a quote of Henry Spencer by Carmack. http://number-none.com/blow/john_carmack_on_inlined_code.html http://number-none.com/blow/john_carmack_on_inlined_code.htm... Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability
    - scrape_it 8y ago
      huh? interesting, do you have more info, I love reading stuff like this. I don't know much about the Gripen but it is my all time favorite after the F-16. Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew: https://www.youtube.com/watch?v=49L9BlYQSjw https://www.youtube.com/watch?v=49L9BlYQSjw
      - mongol 8y ago
        The first crash: https://www.youtube.com/watch?v=k6yVU_yYtEc https://www.youtube.com/watch?v=k6yVU_yYtEc Second crash (over middle of Stockholm) https://youtu.be/mkgShfxTzmo?t=133 https://youtu.be/mkgShfxTzmo?t=133 From Wikipedia: During the test programme, concern surfaced about the aircraft's avionics, specifically the fly-by-wire flight control system (FCS), and the relaxed stability design. On 2 February 1989, this issue led to the crash of the prototype during an attempted landing at Linköping; the test pilot Lars Rådeström walked away with a broken elbow. The cause of the crash was identified as pilot-induced oscillation, caused by problems with the FCS's pitch-control routine.[22][33][34] In response to the crash Saab and US firm Calspan introduced software modifications to the aircraft. A modified Lockheed NT-33A was used to test these improvements, which allowed flight testing to resume 15 months after the accident. On 8 August 1993, production aircraft 39102 was destroyed in an accident during an aerial display in Stockholm. Test pilot Rådeström lost control of the aircraft during a roll at low altitude when the aircraft stalled, forcing him to eject. Saab later found the problem was high amplification of the pilot's quick and significant stick command inputs. The ensuing investigation and flaw correction delayed test flying by several months, resuming in December 1993.[22]
tluyben2 8y ago
It would ensure people thought about it a lot longer and harder than without those proofs, so the code had a whole lot more critical thinking done over it. Seems worth it in some areas like airplanes.
- mikeash 8y ago
  The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” and ended up with the exact same result. A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.
  - tluyben2 8y ago
    Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.
    - mikeash 8y ago
      I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.
      - tluyben2 8y ago
        Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered. I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.
umvi 8y ago
Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements. You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!). Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well! I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.
- AnimalMuppet 8y ago
  This. MCAS was the wrong thing to build. The wrong thing, correctly built, is still wrong, no matter how perfect the formal verification.
  - no-s 8y ago
    So true. The problem is in the system at a higher level. It is not really a software defect that killed all those folks.
zestyping 8y ago
If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verify the software itself, so how does that help?
- crimsonalucard 7y ago
  In a type checked language. Your software is guaranteed to have no type errors. How hard was that?
  - zestyping 7y ago
    That's a great example! It illustrates the point in a better way than I tried to. A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself. If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.

by bollu 8y ago

crimsonalucard 8y ago

No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.

scrape_it 8y ago
Well, to support the top parent's comment, here's what John Carmack had to say about SAAB's fighter jet: > The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling it what to do, but this worked out well for testing: all data was allocated statically, and monitoring those variables gave a clear picture of most everything the software was doing. The software did only the bare essentials, and of course, they were serious about thorough ground testing. > No bug has ever been found in the “released for flight” versions of that code. so not quite that tests are useless because blackbox, but more that yes, it is possible to write software that facilitates showing a code will do what it says it will do. In another note, I do feel sorry for the engineers but at the same time Airbus also has similar MCAS system, but the only thing that saves them is an extra Angle-of-Attack sensor whereas I believe the boeing relied on just one or two. Airbus had 3 AOA sensors and if 2 agreed, that was the data fed into the MCAS. It still boggles my mind that they would place a bigger engine when the original plane was not built for it at all, this was 100% profit orientated move to prevent Airbus from taking Boeing's majority marketshare, it's highly ironic that the opposite results. Even more infuriating is that Boeing passed it off as the exact same plane, not much extra training is necessary, along with FAA giving their blessing, now caught up in the mess. Canada for instance is now looking to the EU for an independent auditing, as any credibility FAA has built up over the past years has taken a significant hit.
- mongol 8y ago
  Interesting quote. Seems it was actually a quote of Henry Spencer by Carmack. http://number-none.com/blow/john_carmack_on_inlined_code.html http://number-none.com/blow/john_carmack_on_inlined_code.htm... Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability
  - scrape_it 8y ago
    huh? interesting, do you have more info, I love reading stuff like this. I don't know much about the Gripen but it is my all time favorite after the F-16. Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew: https://www.youtube.com/watch?v=49L9BlYQSjw https://www.youtube.com/watch?v=49L9BlYQSjw
    - mongol 8y ago
      The first crash: https://www.youtube.com/watch?v=k6yVU_yYtEc https://www.youtube.com/watch?v=k6yVU_yYtEc Second crash (over middle of Stockholm) https://youtu.be/mkgShfxTzmo?t=133 https://youtu.be/mkgShfxTzmo?t=133 From Wikipedia: During the test programme, concern surfaced about the aircraft's avionics, specifically the fly-by-wire flight control system (FCS), and the relaxed stability design. On 2 February 1989, this issue led to the crash of the prototype during an attempted landing at Linköping; the test pilot Lars Rådeström walked away with a broken elbow. The cause of the crash was identified as pilot-induced oscillation, caused by problems with the FCS's pitch-control routine.[22][33][34] In response to the crash Saab and US firm Calspan introduced software modifications to the aircraft. A modified Lockheed NT-33A was used to test these improvements, which allowed flight testing to resume 15 months after the accident. On 8 August 1993, production aircraft 39102 was destroyed in an accident during an aerial display in Stockholm. Test pilot Rådeström lost control of the aircraft during a roll at low altitude when the aircraft stalled, forcing him to eject. Saab later found the problem was high amplification of the pilot's quick and significant stick command inputs. The ensuing investigation and flaw correction delayed test flying by several months, resuming in December 1993.[22]

tluyben2 8y ago

It would ensure people thought about it a lot longer and harder than without those proofs, so the code had a whole lot more critical thinking done over it. Seems worth it in some areas like airplanes.

mikeash 8y ago
The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” and ended up with the exact same result. A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.
- tluyben2 8y ago
  Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.
  - mikeash 8y ago
    I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.
    - tluyben2 8y ago
      Well, yes. But, and who knows if it is true, but you would think you can think up that you need sensor errors to be tested and maybe figure out you need three errors vs two for instance to cover all cases; formal systems can help you model and reason about that and come up with cases that are not covered. I think the point is which these disasters show, and some others in the past (was there not a recalled Japanese car with a software issue?) that a few million more for the right resources will save you a lot more down the line. Problem is that this is not really a statement we can prove for formal verification because we do not have enough to compare with; i have a very strong feeling it will make quite a significant difference; if not for the proofs themselves then for the sheer number of hours and time the proofwriters thought about it by the time of delivery.

umvi 8y ago

Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements. You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!). Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well! I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.

AnimalMuppet 8y ago
This. MCAS was the wrong thing to build. The wrong thing, correctly built, is still wrong, no matter how perfect the formal verification.
- no-s 8y ago
  So true. The problem is in the system at a higher level. It is not really a software defect that killed all those folks.

zestyping 8y ago

If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verify the software itself, so how does that help?

crimsonalucard 7y ago
In a type checked language. Your software is guaranteed to have no type errors. How hard was that?
- zestyping 7y ago
  That's a great example! It illustrates the point in a better way than I tried to. A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself. If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.