5 ms·

The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blac

The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.

jsiepkes 8y ago
Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.
- crimsonalucard 8y ago
  No, we can literally prove it correct based off of a specification. https://en.wikipedia.org/wiki/Correctness_(computer_science) https://en.wikipedia.org/wiki/Correctness_(computer_science) In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.
  - softwaredoug 8y ago
    Yeah and then the specification at that level of specificity IS the code. How do you prove the specification is bug free?
    - crimsonalucard 8y ago
      Define what is a bug in a spec? I defined the program to do one thing and one thing only. What does does it mean when I have a bug in my definition? There's a definition for the definition? Makes no sense.
      - aassddffasdf 8y ago
        It means that the one thing you defined it to do was not the right thing.
      - throwaway2048 8y ago
        You can argue that no code ever has bugs by that logic, after all you defined the program to do one thing, and it did it, it was merely human expectation that was in error.
        crimsonalucard 8y ago
        That's what I'm arguing. Code can be proven correct against a formal spec. However, because we don't do proofs in software, there are bugs.
        throwaway2048 8y ago
        Code is itself a specification.
        crimsonalucard 8y ago
        It can be, but generally it is not.
  - tluyben2 8y ago
    If the spec is complex you are probably proving the bugs in the spec are indeed correctly implemented... Edit: that said, spending the formal spec time will probably reduce the number of bugs far below than what we find normal now. But money...
  - AnimalMuppet 8y ago
    > Bugs can arise where programs intersect in the real world. Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness. But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)
    - crimsonalucard 8y ago
      You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.
mehrdadn 8y ago
Isn't digital logic testing a thing for hardware?
- Gibbon1 8y ago
  Complex hardware often contains bugs many of which map to software bugs. Hardware though tends to be highly constrained in how it's operated. Man: Doc it hurts when I bend my knee this way. Doc: Well don't do that. EE: The hardware state machine runs into the weeds when given these inputs. Tech Rep: Yeah don't do that.
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.
alacombe 8y ago
Proving something is correct is only part of the problem. A random bit flip (no matter amount of error correction and physical hardening) and your proven-correct software goes amok. And this is just one of the many issue you can encounter dealing with the physical world.
- crimsonalucard 8y ago
  Yeah, you're right. Can't completely get rid of tests but the irony still exists.
- samatman 8y ago
  Ironically, the solution to this in spacecraft, where radiation is a given, is 2 of 3 with polling. The system which should have been using for attitude detection in the 737 MAX, and wasn't.
  - throwaway2048 8y ago
    Dosen't eliminate a single point of failure, after all a bitflip in the voting mechanism can also result in error.
WalterBright 8y ago
Proving that software matches the spec is one thing, proving that the spec is free of bugs is quite another.
- bdamm 8y ago
  Indeed. It is normal that implementation will find a bug in the spec. Anecdotally, have never found a flawless RFC. Every real-world implementation of an RFC I've ever done has found some discrepancy when it came to compatibility testing.
- crimsonalucard 8y ago
  Yes. But for critical software systems, what excuse does one have not to prove that the software does not match the spec. There is no excuse not to test the spec, but what excuse is there not to prove the software?
teddyh 8y ago
I refer you to Joel Spolsky about formal proofs of programs: […] So in the first day of that class, Dr. Zuck filled up two entire whiteboards and quite a lot of the wall next to the whiteboards proving that if you have a light switch, and the light was off, and you flip the switch, the light will then be on. The proof was insanely complicated, and very error-prone. It was harder to prove that the proof was correct than to convince yourself of the fact that switching a light switch turns on the light. Indeed the multiple whiteboards of proof included many skipped steps, skipped because they were too tedious to go into formally. Many steps were reached using the long-cherished method of Proof by Induction, others by Proof by Reductio ad Absurdum, and still others using Proof by Graduate Student. For our homework, we had to prove the converse: if the light was off, and it’s on now, prove that you flipped it. I tried, I really did. I spent hours in the library trying. After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, this mechanism would never be able to prove things that are interesting. https://www.joelonsoftware.com/2005/01/02/advice-for-computer-science-college-students/ https://www.joelonsoftware.com/2005/01/02/advice-for-compute...
- nextos 8y ago
  I have a MSc in formal methods, and this is really misleading. Surely you cannot make some proofs easily. However, how did Airbus verify that some errors simply do not exist in their fly-by-wire software (which is ~100 KLOC implemented in a subset of C)? (I'm sure Boeing also employs these techniques internally). Using abstract interpretation. There are tons of formal methods, ranging from type systems to formal proofs. Lots of compromises can be made to make them practical and useful for a particular domain. Look into [1,2] for some quick introductory examples. Going straight into formal proofs is in general a really bad idea. I have worked on railway control systems, with really nasty potential race conditions and managed to prove the absence of large classes of errors. Then derived implementations formally. It's really not that hard. There's even a subfield of CS looking into verifying formal properties of biological systems [3], which are really complex. [1] http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ [2] http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ [3] http://lucacardelli.name/Papers/Abstract%20Machines%20of%20Systems%20Biology%20%28Draft%29.pdf http://lucacardelli.name/Papers/Abstract%20Machines%20of%20S...
threatofrain 8y ago
Mathematicians often don't rely on the exact correctness of a proof's description, instead relying on a rough sketch of strategy.

The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.

jsiepkes 8y ago

Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.

crimsonalucard 8y ago
No, we can literally prove it correct based off of a specification. https://en.wikipedia.org/wiki/Correctness_(computer_science) https://en.wikipedia.org/wiki/Correctness_(computer_science) In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.
- softwaredoug 8y ago
  Yeah and then the specification at that level of specificity IS the code. How do you prove the specification is bug free?
  - crimsonalucard 8y ago
    Define what is a bug in a spec? I defined the program to do one thing and one thing only. What does does it mean when I have a bug in my definition? There's a definition for the definition? Makes no sense.
    - aassddffasdf 8y ago
      It means that the one thing you defined it to do was not the right thing.
    - throwaway2048 8y ago
      You can argue that no code ever has bugs by that logic, after all you defined the program to do one thing, and it did it, it was merely human expectation that was in error.
      - crimsonalucard 8y ago
        That's what I'm arguing. Code can be proven correct against a formal spec. However, because we don't do proofs in software, there are bugs.
        throwaway2048 8y ago
        Code is itself a specification.
        crimsonalucard 8y ago
        It can be, but generally it is not.
- tluyben2 8y ago
  If the spec is complex you are probably proving the bugs in the spec are indeed correctly implemented... Edit: that said, spending the formal spec time will probably reduce the number of bugs far below than what we find normal now. But money...
- AnimalMuppet 8y ago
  > Bugs can arise where programs intersect in the real world. Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness. But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)
  - crimsonalucard 8y ago
    You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.

mehrdadn 8y ago

Isn't digital logic testing a thing for hardware?

Gibbon1 8y ago
Complex hardware often contains bugs many of which map to software bugs. Hardware though tends to be highly constrained in how it's operated. Man: Doc it hurts when I bend my knee this way. Doc: Well don't do that. EE: The hardware state machine runs into the weeds when given these inputs. Tech Rep: Yeah don't do that.

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.

alacombe 8y ago

Proving something is correct is only part of the problem. A random bit flip (no matter amount of error correction and physical hardening) and your proven-correct software goes amok. And this is just one of the many issue you can encounter dealing with the physical world.

crimsonalucard 8y ago
Yeah, you're right. Can't completely get rid of tests but the irony still exists.
samatman 8y ago
Ironically, the solution to this in spacecraft, where radiation is a given, is 2 of 3 with polling. The system which should have been using for attitude detection in the 737 MAX, and wasn't.
- throwaway2048 8y ago
  Dosen't eliminate a single point of failure, after all a bitflip in the voting mechanism can also result in error.

WalterBright 8y ago

Proving that software matches the spec is one thing, proving that the spec is free of bugs is quite another.

bdamm 8y ago
Indeed. It is normal that implementation will find a bug in the spec. Anecdotally, have never found a flawless RFC. Every real-world implementation of an RFC I've ever done has found some discrepancy when it came to compatibility testing.
crimsonalucard 8y ago
Yes. But for critical software systems, what excuse does one have not to prove that the software does not match the spec. There is no excuse not to test the spec, but what excuse is there not to prove the software?

teddyh 8y ago

I refer you to Joel Spolsky about formal proofs of programs: […] So in the first day of that class, Dr. Zuck filled up two entire whiteboards and quite a lot of the wall next to the whiteboards proving that if you have a light switch, and the light was off, and you flip the switch, the light will then be on. The proof was insanely complicated, and very error-prone. It was harder to prove that the proof was correct than to convince yourself of the fact that switching a light switch turns on the light. Indeed the multiple whiteboards of proof included many skipped steps, skipped because they were too tedious to go into formally. Many steps were reached using the long-cherished method of Proof by Induction, others by Proof by Reductio ad Absurdum, and still others using Proof by Graduate Student. For our homework, we had to prove the converse: if the light was off, and it’s on now, prove that you flipped it. I tried, I really did. I spent hours in the library trying. After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, this mechanism would never be able to prove things that are interesting. https://www.joelonsoftware.com/2005/01/02/advice-for-computer-science-college-students/ https://www.joelonsoftware.com/2005/01/02/advice-for-compute...

nextos 8y ago
I have a MSc in formal methods, and this is really misleading. Surely you cannot make some proofs easily. However, how did Airbus verify that some errors simply do not exist in their fly-by-wire software (which is ~100 KLOC implemented in a subset of C)? (I'm sure Boeing also employs these techniques internally). Using abstract interpretation. There are tons of formal methods, ranging from type systems to formal proofs. Lots of compromises can be made to make them practical and useful for a particular domain. Look into [1,2] for some quick introductory examples. Going straight into formal proofs is in general a really bad idea. I have worked on railway control systems, with really nasty potential race conditions and managed to prove the absence of large classes of errors. Then derived implementations formally. It's really not that hard. There's even a subfield of CS looking into verifying formal properties of biological systems [3], which are really complex. [1] http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/ [2] http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ [3] http://lucacardelli.name/Papers/Abstract%20Machines%20of%20Systems%20Biology%20%28Draft%29.pdf http://lucacardelli.name/Papers/Abstract%20Machines%20of%20S...

threatofrain 8y ago

Mathematicians often don't rely on the exact correctness of a proof's description, instead relying on a rough sketch of strategy.