After finishing this book it struck me that it's helplessly Americentric; such giants of the field as Thierry Coquand and Gérard Huet, the entire COQ project, the notion of a "logical framework" (thank you Gordon Plotkin and friends), and sundry other influential things fail to rate a mention. (OK, Per Martin-Löf gets a guernsey as the godfather of neo-constructivism, though the entire Swedish-west-coast movement he inspired goes unremarked.) The problem of having to manually provide variable instantiations (due to the undecidability of higher-order unification) is alluded to (p270), but where is the follow-up pointer to the pragmatic resolution used in e.g. Isabelle, with linear patterns, stylised rules and all that?
The continual reference to the issue of proof and to mathematical practice as normative or indicative is misleading; the issue is how to engineer computer systems as rigorously as we do other artefacts, such as bridges and planes, and most of the epistemological issues involved are not unique to computer science. Similarly we need not think of these proof assistants as oracles so much as mechanisations of other people's expertise, in much the same way that structured programming and libraries (or even design patterns if you like that sort of thing) guide us towards best-practice, and employing algebraic structures leads to all sorts of nice things, like compositionality.
Putting it another way, why would one ever think that a computer system can be engineered to be more reliable than a motor car?
Still, the book does have some interesting discussions on just what a proof is. John Barwise's conception of formal proof as an impoverished subclass of mathematical proof rings true to me, though the particular example (p324):
... [C]onsider proofs where one establishes one of several cases and then observes that the others follow by symmetry considerations. This is a perfectly valid (and ubiquitous) form of mathematical reasoning, but I know of no system of formal deduction that admits such a general rule.
is a bit weak: in Isabelle, one could prove a case, prove that the others are in fact symmetric variants of it, then draw the conclusion. If the symmetry proof were abstract enough it could be enshrined in a library.