A futuristic scenario, in which Usain Bolt, partakes in "Space Olympics", because of advancements in human technology, like space suits, and gravity flying boots
I get your point, how long do we keep digging before we reach the center of the earth?
It is human nature to quit, most especially, when there is no foreseeable benefits.
But think about it this way, science is like the human body.
The head of science, are those scientists who make a new discovery by going through research articles of their predescessors, who were just 1 mm from digging up gold.
The necks are those scientists, who almost made a new discovery, but couldn't see the light at the end of the tunnel.
And the legs, are the early scientist like Galileo, who laid the ground work.
Anyways, wherever you find yourself, it is imperative you don't lose faith in the process.
Afterall, everybody mocked the Wright brothers, for building a plane. And most advanced scientist question, why they venture into this field called science, afterall it is a labor of love, and only the lucky few get glorified.
But I get your point through and through, it is better scientists pour in their brains in more linear science, like things we can see and computate, instead of pouring brain power in abstract concept that has no current benefit in the present society.
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.
> 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.
