Dijkstra on Dutch TV (2000)

Re:Dijkstra on Dutch TV (2000) by dkarapetyan on Sunday May 25, 2014 @04:51AM (#7795857)

That's the standard narrative and parroting it over and over again doesn't really make it true. Arguments over correctness almost always devolve into a shouting match because no one ever defines what they mean by it. For your standard consumer application a notion of correctness doesn't even exist so the argument is moot there. You have to narrow your domain a little bit to actually start talking about it. You have to get down to the level of protocols and interfaces and other mathematical beasts where correctness actually means something.

The standard example of correct software and in fact where most work on formal correctness tends to happen is in compiler design and distributed systems. So when you say that there is a tradeoff between speed and correctness that is simply not true. All those compilers you use are correct, for a very precise definition of correct, and fast and constantly improving.

[ Parent | on HN ]

Re:Dijkstra on Dutch TV (2000) by gw on Sunday May 25, 2014 @01:37PM (#7796908)

We weren't arguing about formal correctness, so I can only assume you have stumbled into the wrong thread. We were discussing whether safety-critical software still involved a tradeoff between lacking bugs (or "errors" as Dijkstra would prefer calling them) and getting finished on time ("speed" in the development sense, not in terms of runtime performance like you seem to have assumed).

I appreciate your concern that a shouting match was imminent, but with gems like "running your mouth" and "parroting it over and over again" I think, ironically, the only one risking that is yourself.

[ Parent | on HN ]

Re:Dijkstra on Dutch TV (2000) by icebraining on Sunday May 25, 2014 @06:02AM (#7795976)

All those compilers you use are correct, for a very precise definition of correct

Are they? How do we know? And if they are, why is GCC's list of major and critical bugs[1], for example, longer than a laundry list?

[1] https://gcc.gnu.org/bugzilla/buglist.cgi?bug_severity=critic...

[ Parent | on HN ]

Re:Dijkstra on Dutch TV (2000) by dkarapetyan on Sunday May 25, 2014 @07:00AM (#7796062)

    Beware of bugs in the above code; I have only proved it correct, not tried it. 
    - Donald Knuth

Formal correctness and implementation correctness are still separate issues in compilers like gcc but that doesn't change the fact that there are correctness specifications for gcc. There are projects that try to bridge the gap: https://en.wikipedia.org/wiki/CompCert.

[ Parent | on HN ]