6 ms·

That was my first thought as well but then I realized that by correctness the author means "no bug", which is quite more ambitious than just making it "work".

That was my first thought as well but then I realized that by correctness the author means "no bug", which is quite more ambitious than just making it "work". I think the author implicitly assumes the software basically works right from the beginning of the article.

kibwen 8y ago
If that's the case then the author is attacking a straw man, because nobody (besides Dijkstra) is suggesting that we rewrite all the software in the world in Coq in order to 100% eliminate bugs at the cost of simplicity.
- KirinDave 8y ago
  That's not what Coq would do, and a misrepresentation of Dijkstra's position. We certainly could use tools like TLA+ to assist us with existing code. Folks are using "simple" and "easy" interchangeably here. That's probably inappropriate.
  - kibwen 8y ago
    I apologize for using Coq speicifically, I just needed a scapegoat for formal verification that people might have actually ever heard of. :P I'm happy to debate definitions, which the author of the OP has regretfully omitted (and the contentious definition here is probably the OP's notion of correctness, rather than their notion of simplicity).
    - KirinDave 8y ago
      To be honest, I'm fine skipping it. I don't understand why this article is so upvoted anyways.
    - AstralStorm 8y ago
      You'd be surprised how simple a well written proof can be compared to a program implementing an algorithm to do the same. That said, Coq itself is not the best vehicle for this. There are nicer high order logic languages.
  - icc97 8y ago
    > Folks are using "simple" and "easy" interchangeably here. That's probably inappropriate. Agreed, see Rich Hickey's "Simplicity Matters" presentation on the difference [0]. Simple-Complex vs Easy-Hard [0]: https://www.youtube.com/watch?v=rI8tNMsozo0 https://www.youtube.com/watch?v=rI8tNMsozo0
silverbax88 8y ago
I agree. What he means is, it should work first, as simply as possible. Then you worry about correctness- correctness is not referring to working/no working. Correctness means, 'how SHOULD this work?' or 'How should this logic or code be written to be most efficient or effective?' Third is performance. 1. Write a working piece of software that does the job. 2. Refactor to make the working piece of software do the job more efficiently and elegantly. 3. Refactor to make the working piece of software do the job as fast as possible.

kibwen 8y ago

If that's the case then the author is attacking a straw man, because nobody (besides Dijkstra) is suggesting that we rewrite all the software in the world in Coq in order to 100% eliminate bugs at the cost of simplicity.

KirinDave 8y ago
That's not what Coq would do, and a misrepresentation of Dijkstra's position. We certainly could use tools like TLA+ to assist us with existing code. Folks are using "simple" and "easy" interchangeably here. That's probably inappropriate.
- kibwen 8y ago
  I apologize for using Coq speicifically, I just needed a scapegoat for formal verification that people might have actually ever heard of. :P I'm happy to debate definitions, which the author of the OP has regretfully omitted (and the contentious definition here is probably the OP's notion of correctness, rather than their notion of simplicity).
  - KirinDave 8y ago
    To be honest, I'm fine skipping it. I don't understand why this article is so upvoted anyways.
  - AstralStorm 8y ago
    You'd be surprised how simple a well written proof can be compared to a program implementing an algorithm to do the same. That said, Coq itself is not the best vehicle for this. There are nicer high order logic languages.
- icc97 8y ago
  > Folks are using "simple" and "easy" interchangeably here. That's probably inappropriate. Agreed, see Rich Hickey's "Simplicity Matters" presentation on the difference [0]. Simple-Complex vs Easy-Hard [0]: https://www.youtube.com/watch?v=rI8tNMsozo0 https://www.youtube.com/watch?v=rI8tNMsozo0

silverbax88 8y ago

I agree. What he means is, it should work first, as simply as possible. Then you worry about correctness- correctness is not referring to working/no working. Correctness means, 'how SHOULD this work?' or 'How should this logic or code be written to be most efficient or effective?' Third is performance. 1. Write a working piece of software that does the job. 2. Refactor to make the working piece of software do the job more efficiently and elegantly. 3. Refactor to make the working piece of software do the job as fast as possible.