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.<p><a href="https://en.wikipedia.org/wiki/Brian_Cantwell_Smith" rel="nofollow">https://en.wikipedia.org/wiki/Brian_Cantwell_Smith</a>.<p>I didn't know any of his other papers. Beautiful.
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.