5 ms·

There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it wou

There is a sense also of merely moving the problem. If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. On the flip side, type systems bring at least some sense of proof into programming.

NovemberWhiskey 3y ago
>If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. That seems like a weird conclusion to me. You definitely can't write a "correct" program unless you know what you expect it to do. It's easier to write a specification than a program, because a specification is at a higher level of semantic abstraction.
- AnimalMuppet 3y ago
  You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
  - NovemberWhiskey 3y ago
    I don't think I did dodge the question. Is it easier to write a correct specification that correct code? Yes, absolutely, because in a specification I can specify outcomes without having to say how they're achieved, and I can specify results that are invariant over time without having to say how they're maintained, etc. A specification is essentially a bridge between, on the one hand, a higher-level requirements document that's probably imprecise and/or contradictory and/or incomplete and, on the other, code that has to be completely deterministic.
    - staunton 3y ago
      I agree with you but still want to play devil's advocate regarding you argument: > [It's easier to write specifications than implementations because] in a specification I can specify outcomes without having to say how they're achieved It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. This way, "correct" isn't a meaningful category, there's only "incorrect in retrospect". This is how most software is made and for most applications I would expect cost-benefit analysis to favor it.
      - NovemberWhiskey 3y ago
        I can easily write a specification for a function that says: given input integer n (n>2) return a vector of integer values (a, b, c) such that a^n + b^n = c^n or return an error if no such value exists. I invite you to write a concise unit test of the implementation of said function!
        AnimalMuppet 3y ago
        assert(vector.is_empty()); ;-)
      - wizzwizz4 3y ago
        > It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. It's even even easier to write a specification that says "if this case, do this; if that case, do that; otherwise, do whatever". Just use your proof language's implication symbol. (this ==> THIS) && (that ==> THAT), done.

NovemberWhiskey 3y ago

>If you can’t write a correct program, can you write a correct specification? For many problem domains it would make little sense even to try. That seems like a weird conclusion to me. You definitely can't write a "correct" program unless you know what you expect it to do. It's easier to write a specification than a program, because a specification is at a higher level of semantic abstraction.

AnimalMuppet 3y ago
You slightly dodged the question. Is it easier to write a correct specification? But I think the answer is still yes, and still because it's at a higher level of abstraction. There are more details to specify in a program, and there can be bugs in that.
- NovemberWhiskey 3y ago
  I don't think I did dodge the question. Is it easier to write a correct specification that correct code? Yes, absolutely, because in a specification I can specify outcomes without having to say how they're achieved, and I can specify results that are invariant over time without having to say how they're maintained, etc. A specification is essentially a bridge between, on the one hand, a higher-level requirements document that's probably imprecise and/or contradictory and/or incomplete and, on the other, code that has to be completely deterministic.
  - staunton 3y ago
    I agree with you but still want to play devil's advocate regarding you argument: > [It's easier to write specifications than implementations because] in a specification I can specify outcomes without having to say how they're achieved It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. This way, "correct" isn't a meaningful category, there's only "incorrect in retrospect". This is how most software is made and for most applications I would expect cost-benefit analysis to favor it.
    - NovemberWhiskey 3y ago
      I can easily write a specification for a function that says: given input integer n (n>2) return a vector of integer values (a, b, c) such that a^n + b^n = c^n or return an error if no such value exists. I invite you to write a concise unit test of the implementation of said function!
      - AnimalMuppet 3y ago
        assert(vector.is_empty()); ;-)
    - wizzwizz4 3y ago
      > It's even easier to write a few "unit tests" that "specify" intended behavior, write code that passes those tests, and then worry what to do in edge-cases when they happen. It's even even easier to write a specification that says "if this case, do this; if that case, do that; otherwise, do whatever". Just use your proof language's implication symbol. (this ==> THIS) && (that ==> THAT), done.