I think this guy just isn't too hot at mathematics. Omitting a trivial step (or domain specific knowledge) is not a lack of rigour, but a courtesy to the reader. The details can always be filled in cleanly.
A very astute comment. In principle, mathematical proofs are supposed to be every bit as completely described as computer programs, but perhaps not as explicitly expressed. Edsger Dijkstra used to refer to mathematical proofs as a model for computer programming.
I'm not a mathematician, but I can imagine some sort of "library of derivation" whereupon, in order to prove something, say, based on arithmetic, you include (the language directive, not the verb) the specification of arithmetic derived in Principia Mathematica. Then the proving system follows your logic to its logic, and then to the logic they relied on, and so on, until everything is completely explicit. Basically, formal execution of bibliographies.
Dijkstra also used to talk about how computing science was a particularly difficult branch of mathematics, basically for the same reason that Vanier is asserting; he recommended that only particularly good mathematicians should switch to computing science, leaving the mediocre mathematicians to what they were already doing.
A very astute comment. In principle, mathematical proofs are supposed to be every bit as completely described as computer programs, but perhaps not as explicitly expressed. Edsger Dijkstra used to refer to mathematical proofs as a model for computer programming.
http://en.wikipedia.org/wiki/Program_derivation