The Limits of Correctness (1985) [pdf] (opens in new tab)

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.

https://en.wikipedia.org/wiki/Brian_Cantwell_Smith.

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.

This is a beautiful text.