I think there is a bit of a disconnect here between the old guard of verification work and the avant-garde. Partly this is a difference of tools and terminology

I think there is a bit of a disconnect here between the old guard of verification work and the avant-garde. Partly this is a difference of tools and terminology—current work in verification has a type-theory feel, and Floyd-style axiomatic semantics are out of vogue. It is also the role of old professors to slowly lose currency with the cutting edge of a field. I wouldn't think too much of Knuth's comments.