“Program testing can be used to create 1 the presence of bugs, but never to show their absence”
1) edited
1) edited
Formal proofs may not be silver bullets, and we’re never safe from a faulty implementation of the proven algorithms, but this quanta article on a DARPA project showed impressive results [0].
There’s also AWS’ use of TLA+ [1].
[0]: https://www.quantamagazine.org/formal-verification-creates-h...
You also aren't safe from misunderstanding what it is that you've proven about the program.
Which is actually the same problem as other software bugs; you have a specification of something, but you don't know what it is that you've specified, and you wish it were something other than what it is.
Interesting to think about a formal code verification system that maintained a connection between all four prime artifacts: natural language description of problem as understood & intended solution, vs. code and the properties actually verified.
Many (most?) non-trivial bugs are actually flaws in the specification, misunderstandings about what exactly you wanted and what real-world consequences arise from what you specified.
And then someone tries it with a ulimit of 16kB.
Does it run?
Do you _know_?
Do you even know what is correct behavior in this situation?
Sugar in the tank is an agreeable example because of how obvious it is, but what about something more subtle? An odd condition that leads to the wrong resonant frequency. An unknown software bug that makes the brakes lock up on Tuesdays at 12:00 AM on one specific backroad in a remote part of Virginia. The combinatorial possibilities of operating conditions are too numerous to exhaustively test.
I guess you could say that every function has every quality that it happens to have, so that functions need only exist in order to be “correct.”