3 ms·

I have proved my code has no bugs according to the spec. I do not make the claim my spec has no bugs.

• deleted 3y ago
  [deleted]
• yasuocidal 3y ago
  "Its not a bug, its a feature"
• coldtea 3y ago
  With formal proof systems, you can also claim that for your spec.
  • svieira 3y ago
    A formal proof is only as good as what-you-are-proving maps to what-you-intended-to-prove.
  • AlotOfReading 3y ago
    I've written formal proofs with bugs more than once. Reality is much messier than you can encode into any proof and there will ultimately be a boundary where the real systems you're trying to build can still have bugs. Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".
  • llm_trw 3y ago
    No you can't. You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invariants the real system must have and that it doesn't violate them in number of steps + 1.
  • cortesoft 3y ago
    This doesn't track with the real world, though. If you are writing software, it is almost always trying to accomplish a goal outside of itself. It is trying to solve a problem for someone, and how that problem can or should be solved is rarely perfectly clear. The spec is supposed to map to a real world problem, and there is never going to be a way to formalize that mapping.