I have been reading a lot lately and I have come across articles in which people make the ‘grand’ assertions that there are no bugs in the Tex program by donald knuth. Is this in any way possible and if so how is this possible?
2
(even though it’s been marked as duplicate, my answer is not 😉
It is possible but no one can prove it, not for TeX size.
http://ertos.nicta.com.au/research/l4.verified/ is an example of a verified piece of software.
There are two things that anyone can do to say that their software is bug free (not saying that Don said it):
- test the hell out of it and fix the bugs until there’s no more bug.
- come up with a proof by formal method.
Problem with (1) is even if a software passed testing, there’s still no proof that there’s no bug. It only proves the program has no bug which would be detected by the set of tests. For large program, the cost of testing would be too high. TeX has enjoyed basically free testing from its user base. If Don could prove that TeX is bug free, he could’ve put a million dollar bounty.
The link I put up there is an example of (2) how a reasonable size program can be proven. By reasonable I mean, it can do something useful, not one line program that has trivial proof. What they’ve done is they’ve designed, refined the design and translated the design to C and had those steps checked by theorem prover (Isabelle/HOL). The size of the proven part is 7500 lines of C code.
Probably it would be too hard to have all programs built as trustworthy system, but it is conceivable to have some parts of a program verified and have tests cover the remaining parts of the program.
2