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?


1 Answer 1


(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):

  1. test the hell out of it and fix the bugs until there's no more bug.
  2. 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.

  • Also what you consider a bug really changes things. For example, is TeX not supporting all UNICODE text a bug for a missing feature? Is running out of memory a bug? Commented Aug 26, 2020 at 10:39
  • 1
    If the software didn't work as per specification, then it's a bug. If TeX is not specified to support Unicode, that's not a bug. But it should be specified that if it received unsupported input then it shall not crash. Same with out of memory, it happens, so it should be specified what the program will do when OOM happens, e.g. exit gracefully instead of escalating privileges. If those were not specified, then it's missing feature.
    – imel96
    Commented Aug 27, 2020 at 1:02

Not the answer you're looking for? Browse other questions tagged or ask your own question.