5 ms·

> You can never prove that software is correct; the best that will ever be possible is that it matches the specification That's a bit like saying "You can neve

by tome 7y ago

> You can never prove that software is correct; the best that will ever be possible is that it matches the specification That's a bit like saying "You can never prove a mathematical result; the best that will ever be possible is a derivation of a conclusion from a hypothesis".

ncmncm 7y ago
No: all you can prove in math is that a conclusion follows from your choice of axioms. That's fine for math, but software is always part of a system that usually has to, you know, do something useful. The spec is only ever an approximation to that. So, consistent is great, as long as you don't confuse it with right.
- tome 7y ago
  Sure, I know what you're saying. It's just that, unless you take a very narrow view of mathematics as solely a pure subject, application of formally-proven mathematics to the real world is subject to exactly the weaknesses that formally-verified software is subject to. I can formally, mathematically, prove the equation for the trajectory of a spacecraft, but if my model is wrong then the spacecraft may crash. There's no hard distinction between mathematical proof and software verification here.
  - ncmncm 7y ago
    I have no problem with saying software may be proven consistent with a spec. But correctness is just an entirely tougher nut. Promising the latter but only delivering the former may be good enough for the journals, but Engineering has a higher standard to meet.
    - tome 7y ago
      Yes, I entirely agree. I'm just saying that despite having a pure branch, mathematics also has an applied branch which is used in engineering, and formally-proven applied mathematics suffers from the exact same risks of misuse as formally-verified software.
      - ncmncm 7y ago
        OK, yes. Applied mathematics has the same sort of gap between model (axioms) and reality as between specification and actual requirements. In both places people confuse the two, and sometimes make unjustified claims for the second from justified confidence in only the first.

by tome 7y ago

ncmncm 7y ago

No: all you can prove in math is that a conclusion follows from your choice of axioms. That's fine for math, but software is always part of a system that usually has to, you know, do something useful. The spec is only ever an approximation to that. So, consistent is great, as long as you don't confuse it with right.

tome 7y ago
Sure, I know what you're saying. It's just that, unless you take a very narrow view of mathematics as solely a pure subject, application of formally-proven mathematics to the real world is subject to exactly the weaknesses that formally-verified software is subject to. I can formally, mathematically, prove the equation for the trajectory of a spacecraft, but if my model is wrong then the spacecraft may crash. There's no hard distinction between mathematical proof and software verification here.
- ncmncm 7y ago
  I have no problem with saying software may be proven consistent with a spec. But correctness is just an entirely tougher nut. Promising the latter but only delivering the former may be good enough for the journals, but Engineering has a higher standard to meet.
  - tome 7y ago
    Yes, I entirely agree. I'm just saying that despite having a pure branch, mathematics also has an applied branch which is used in engineering, and formally-proven applied mathematics suffers from the exact same risks of misuse as formally-verified software.
    - ncmncm 7y ago
      OK, yes. Applied mathematics has the same sort of gap between model (axioms) and reality as between specification and actual requirements. In both places people confuse the two, and sometimes make unjustified claims for the second from justified confidence in only the first.