Holy crap, I knew that name ringed a bell. At first I confused him with Brian Cantrill (dtrace et al. fame)... but this is Brian C. Smith of 3-Lisp reflective tower interpreter.
As a primer on the many and significant difficulties of analytical verification, this may have some merit; as an argument for the futility of attempting to do so, it depends on a false all-or-nothing dichotomy.