Hacker News Reader

Comment by earedpiece | Hacker News Reader

But from a scientific standpoint, do you think a software can be 100% correct? Bugs will eventually be found.

The best bet, when writing (100%) correct code, is through thorough testing, and hoping for the best, because when you are handling a million lines of code, errors, will definitely creep up.

Personally, I feel achieving a 100% correct code is impossible, since developers are always updating, and adding new features to the code.

Hence why a team, should be put in place to create patches quickly, when bugs are found.

View on HN

> But from a scientific standpoint, do you think a software can be 100% correct?

Sure it can. I've written 100% correct code using Coq. For example, I wrote a relatively simple program (~1.7k LoC) to interpret a simple programming language, but it was definitely correct (certified by a machine-checked proof).

Of course, for larger programs it's much harder to do that. But it's just a matter of how much time you're willing to invest.

On some level, that's sort of like asking whether we can be 100% sure that the solution to a math problem is correct. I mean, I'm pretty sure that 2+3=5, but what if I made a mistake somewhere? What if I'm falling prey to some cognitive bias that makes me blind to certain math errors? What if all of humanity is wrong about this math problem?

If we can be convinced that we're 100% sure that 2+3=5, then what about a more complicated problem? What's the most complex math problem we can be sure about? What if we have to use a computer to check its correctness?

(In general, I think it's usually good enough to say we're pretty sure something is correct if we have some solid basis for believing that it is. I'm okay with being 99.99% sure that 2+3=5, but in the world of software "I'm 50% sure this software is correct" is a standard that most software I use on a daily basis fails to meet.)

CompCert is an example of 100% proven correct software. There are other examples out there. Verification tools are getting better every day, making it less costly to prove code correct.

Reply on news.ycombinator.com