6 ms·

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.

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.