4 ms·

Software can be verified to be correct, stupidity of others is unavoidable.

by Huh1337 4y ago

P5fRxh5kUvp2th 4y ago
Did someone solve the halting problem while I wasn't looking?
- Huh1337 4y ago
  No, but somebody created type checking, linting and testing. Not sure what's up with the CS people and their halting problem. In the industry we've solved (as in developed ways to deal with) the problem of verification decades ago. Also, debuggers. Nobody said the verification can't be done by a human.
  - P5fRxh5kUvp2th 4y ago
    verifying software is correct implies solving the halting problem. What you mean is "no known bugs", so may be use those words instead. "verification of correctness" has a specific meaning in our industry. yeah yeah, I get it, those stupid CS people and their P=NP talk. Don't they know you can obviously verify correctness without verifying it for all possible inputs? What next, you can't prove a negative such as absence of bugs?!?
    - applejacks 4y ago
      > verifying software is correct implies solving the halting problem. No, producing a program that can verify that all correct programs are correct implies solving the halting problem. Verifying a particular piece of software is correct just implies you've proved that one piece correct. (And probably wasted your time dicking around with it only to find that the actual issue was in software you treated as 'outside' of the software you were verifying...)
      - P5fRxh5kUvp2th 4y ago
        What you're describing is the programming version of approximation. It's understood that it has a margin of error due to the approximation. What you're claiming here is that if you check enough inputs you've proven it correct, and what I'm telling you is that's not the case. The fact is, nothing has been proven, the wording on the webpage itself is more honest (no known bugs and a suite of automated tests). To verify a program is correct is a much stronger claim than what is even on the website. And that requires restricting the input or solving the halting problem.

Software can be verified to be correct, stupidity of others is unavoidable.

P5fRxh5kUvp2th 4y ago

Did someone solve the halting problem while I wasn't looking?

Huh1337 4y ago
No, but somebody created type checking, linting and testing. Not sure what's up with the CS people and their halting problem. In the industry we've solved (as in developed ways to deal with) the problem of verification decades ago. Also, debuggers. Nobody said the verification can't be done by a human.
- P5fRxh5kUvp2th 4y ago
  verifying software is correct implies solving the halting problem. What you mean is "no known bugs", so may be use those words instead. "verification of correctness" has a specific meaning in our industry. yeah yeah, I get it, those stupid CS people and their P=NP talk. Don't they know you can obviously verify correctness without verifying it for all possible inputs? What next, you can't prove a negative such as absence of bugs?!?
  - applejacks 4y ago
    > verifying software is correct implies solving the halting problem. No, producing a program that can verify that all correct programs are correct implies solving the halting problem. Verifying a particular piece of software is correct just implies you've proved that one piece correct. (And probably wasted your time dicking around with it only to find that the actual issue was in software you treated as 'outside' of the software you were verifying...)
    - P5fRxh5kUvp2th 4y ago
      What you're describing is the programming version of approximation. It's understood that it has a margin of error due to the approximation. What you're claiming here is that if you check enough inputs you've proven it correct, and what I'm telling you is that's not the case. The fact is, nothing has been proven, the wording on the webpage itself is more honest (no known bugs and a suite of automated tests). To verify a program is correct is a much stronger claim than what is even on the website. And that requires restricting the input or solving the halting problem.