3 ms·

The previous poster is correct. Software cannot be proven to be bug-free. This was considered axiomatic when I worked at IBM as a mainframe programmer on softwa

The previous poster is correct. Software cannot be proven to be bug-free. This was considered axiomatic when I worked at IBM as a mainframe programmer on software that ran ATM machines, Social Security checks, etc. You should definitely read up on the halting problem.

masklinn 8y ago
Software can absolutely be proved bug free. By being proved. Software can not be proved bug-free by tests (and even that assertion is not completely true, you can prove software through exhaustive testing if it's very very simple).
- mimixco 8y ago
  You can't come up with enough tests to prove that software is bug-free. No program has ever been written which is bug-free.
  - masklinn 8y ago
    > You can't come up with enough tests to prove that software is bug-free. Sure you can: you can prove software is correct through exhaustive testing. As noted previously it only works for small input space and simple programs (functions, really) but it does work, you can prove that a boolean xor is correct by enumerating its 4 inputs and checking that all of them produce the expected output. This method can be applied to input spaces up to about 40 bits or so: https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
    - mimixco 8y ago
      I'm talking about real world software. It's unlikely that anyone cares if a Hello World program is bug-free.
      - masklinn 8y ago
        > I'm talking about real world software. What an unexpected coincidence, so am I! > It's unlikely that anyone cares if a Hello World program is bug-free. Did you consider reading the link I provided at any point?
        mimixco 8y ago
        I did read it. I stick by my assertion. In practice, software cannot be proven to be bug free. This assertion has been borne out by numerous companies with nearly unlimited budgets who continue to find severe bugs in their software, despite extensive testing. While it's interesting academically that a single function could be tested and shown to be bug-free, it's not relevant in practice. It's the interaction of multiple functions and subsystems that leads to many bugs -- and inputs in edge cases lead to even more than that.
        masklinn 8y ago
        > I stick by my assertion. In practice, software cannot be proven to be bug free. You can't "stick by your assertion" then provide something which has almost no relation to your original assertion, that's called "moving the goalposts". This moving of goalposts is even more asinine when you're moving them exactly where the comment which you originally decried had put them. Reminder: here is what you originally felt you needed to note was wrong: > Software can not be proved bug-free by tests (and even that assertion is not completely true, you can prove software through exhaustive testing if it's very very simple).
piano 8y ago
> The previous poster is correct. Software cannot be proven to be bug-free. Yes, it can, that's what the whole formally verified software branch is about. Of course, even with formally verified software, there can be failures caused by external factors such as faults in hardware etc. But some piece of software itself absolutely can be proved to be correct (ie. bug-free). It just takes special approaches such as programming languages amenable to formal proofs (eg. Idris). Software is usually written in bug-inducing ways and using languages that hinder formal verification not because provably bug-free software is impossible but because it is typically too costly and difficult to write.
- Izkata 8y ago
  The thing that's always bothered me about this argument is the translation between proof and code+underlying system. Bugs can still be introduced there. Certainly significantly fewer bugs in the final result, but I don't think I'd be confident in calling it proven 100% bug-free.
  - piano 8y ago
    In languages with termination analysis and dependent types, the source code _is_ the proof and it's verified by the compiler. Basically when such a program compiles, it's proved to be correct according to the specification. Of course this still leaves space for bugs outside the program itself which still may influence it, such as bugs in the operating system or firmware or the like. Which may be prevented by having a formally verified OS too :) But even in such a case, there might still be hardware errors (electrical noise, for example). Which is why for example spacecrafts or critical industry machinery double or triple their whole architectures. In such case the formally verified software runs on eg. three instances simulatenously and these instances cross-check each other's results all the time. When a hardware fault occurs (a bit randomly flipped in memory for example), they find out they're not matching and re-calculate. That's as close as you can get to zero bugs.

masklinn 8y ago

Software can absolutely be proved bug free. By being proved. Software can not be proved bug-free by tests (and even that assertion is not completely true, you can prove software through exhaustive testing if it's very very simple).

mimixco 8y ago
You can't come up with enough tests to prove that software is bug-free. No program has ever been written which is bug-free.
- masklinn 8y ago
  > You can't come up with enough tests to prove that software is bug-free. Sure you can: you can prove software is correct through exhaustive testing. As noted previously it only works for small input space and simple programs (functions, really) but it does work, you can prove that a boolean xor is correct by enumerating its 4 inputs and checking that all of them produce the expected output. This method can be applied to input spaces up to about 40 bits or so: https://randomascii.wordpress.com/2014/01/27/theres-only-four-billion-floatsso-test-them-all/ https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
  - mimixco 8y ago
    I'm talking about real world software. It's unlikely that anyone cares if a Hello World program is bug-free.
    - masklinn 8y ago
      > I'm talking about real world software. What an unexpected coincidence, so am I! > It's unlikely that anyone cares if a Hello World program is bug-free. Did you consider reading the link I provided at any point?
      - mimixco 8y ago
        I did read it. I stick by my assertion. In practice, software cannot be proven to be bug free. This assertion has been borne out by numerous companies with nearly unlimited budgets who continue to find severe bugs in their software, despite extensive testing. While it's interesting academically that a single function could be tested and shown to be bug-free, it's not relevant in practice. It's the interaction of multiple functions and subsystems that leads to many bugs -- and inputs in edge cases lead to even more than that.
        masklinn 8y ago
        > I stick by my assertion. In practice, software cannot be proven to be bug free. You can't "stick by your assertion" then provide something which has almost no relation to your original assertion, that's called "moving the goalposts". This moving of goalposts is even more asinine when you're moving them exactly where the comment which you originally decried had put them. Reminder: here is what you originally felt you needed to note was wrong: > Software can not be proved bug-free by tests (and even that assertion is not completely true, you can prove software through exhaustive testing if it's very very simple).

piano 8y ago

> The previous poster is correct. Software cannot be proven to be bug-free. Yes, it can, that's what the whole formally verified software branch is about. Of course, even with formally verified software, there can be failures caused by external factors such as faults in hardware etc. But some piece of software itself absolutely can be proved to be correct (ie. bug-free). It just takes special approaches such as programming languages amenable to formal proofs (eg. Idris). Software is usually written in bug-inducing ways and using languages that hinder formal verification not because provably bug-free software is impossible but because it is typically too costly and difficult to write.

Izkata 8y ago
The thing that's always bothered me about this argument is the translation between proof and code+underlying system. Bugs can still be introduced there. Certainly significantly fewer bugs in the final result, but I don't think I'd be confident in calling it proven 100% bug-free.
- piano 8y ago
  In languages with termination analysis and dependent types, the source code _is_ the proof and it's verified by the compiler. Basically when such a program compiles, it's proved to be correct according to the specification. Of course this still leaves space for bugs outside the program itself which still may influence it, such as bugs in the operating system or firmware or the like. Which may be prevented by having a formally verified OS too :) But even in such a case, there might still be hardware errors (electrical noise, for example). Which is why for example spacecrafts or critical industry machinery double or triple their whole architectures. In such case the formally verified software runs on eg. three instances simulatenously and these instances cross-check each other's results all the time. When a hardware fault occurs (a bit randomly flipped in memory for example), they find out they're not matching and re-calculate. That's as close as you can get to zero bugs.