4 ms·

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 spec

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.

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.