Simple, correct, fast: in that order

Re:Simple, correct, fast: in that order by KirinDave on Monday July 09, 2018 @11:34AM (#17490988)

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.

[ Parent | on HN ]

Re:Simple, correct, fast: in that order by kibwen on Monday July 09, 2018 @11:40AM (#17491031)

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).

[ Parent | on HN ]

Re:Simple, correct, fast: in that order by AstralStorm on Monday July 09, 2018 @01:02PM (#17491679)

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.

[ Parent | on HN ]

Re:Simple, correct, fast: in that order by KirinDave on Monday July 09, 2018 @12:04PM (#17491240)

To be honest, I'm fine skipping it. I don't understand why this article is so upvoted anyways.

[ Parent | on HN ]

Re:Simple, correct, fast: in that order by icc97 on Monday July 09, 2018 @05:47PM (#17493711)

> 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

[ Parent | on HN ]