From: "Fred lunnon" <fred.lunnon@gmail.com>

Anyone who has attempted seriously to program mathematical algorithms for computer [an activity almost co-extensive with theorem- proving] will be aware of the pleasurable momentary surge of astonishment when a progam of --- say --- ten lines or so apparently works at the first attempt; not to mention the familiar incredulous frustration when closer investigation establishes that it in practice still fails to do after the tenth.

It follows that any proof published at the research level is almost certainly technically incorrect --- even discounting failures at the "typographical" level, which might be dismissed as amenable to an informed reader's error-correction facility.

_The Elements of Programming Style_, by Kernighan and Plauger, famously headed its sections with examples of bad style taken from other textbooks. I'm not sure whether it was that book, or maybe one of these: _Software Tools_ by Kernighan, _Structure and Interpretation of Computer Programs_, by Ableson, Sussman and Sussman or ? ...which boasted that every code example was automatically tested by a script that extracted it from the source text as sent to the typesetting software. Looking at SICP, there are a lot of exercises asking you to debug pieces of code. Sussman's PhD thesis was on a program that wrote incorrect programs and tried to fix them. --Steve