Dijkstra on Dutch TV (2000)

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 ]