alt Hacker News>Grandparent is onto something. You can't define correctness without a spec.
Sure you can. Correctness doesn't mean "follows a spec", it means "It does what the developer intended it to do without problems".
I mean that casually and within reason, it's not supposed to be a formal statement checkable by proof checker. z
I don't need a spec to know that e.g. my email client has a bug if it crashes when I try to make something bold. The presense of the "Bold" formatting button means it should support it, spec or no spec.
I did not mention 'formal statement checkable by proof checker' anywhere. Correctness requires some criterion external to the implementation. Write it down and it's a spec. If you do not write it down and the behaviour is not one of the already-standard failure classes like crashing, corrupting data, losing work, then there is no principled way to classify it as a bug rather than an intended feature or tradeoff.