A reference peeve

One thing has been peeving me for a while. It is small and does not impact me directly, so I didn't speak up, but perhaps I should.

Many people, some of whom should know better, mention Floyd, Hoare and Dijkstra in the same sentence as modern verification condition generators (Frama-C's Wp plug-in, Frama-C's Jessie plug-in, Microsoft Research's VCC, ...) as if there was nothing in between the writings of these great men and those tools.

ACSL By Example by example has a "The Hoare Calculus" section with rules that are close to some old publication from one of these three authors. It gives an intuition of how Jessie and now Wp work but you have to realize that these are not the rules that these tools actually use not by a far shot.

It is one of the creators of modern verification generators' achievements that their verifiers work so well you don't notice they aren't using the simple intuitive rules. They aren't and if they were you would notice. If you are a pragmatist and want to feel the difference between this and that try making classical Hoare logic rules work to compute the actual weakest precondition for this simple C function and work your way up from there.

Implying that modern verification condition generators are direct applications of the work of Floyd Hoare and Dijkstra is akin to walking to say one of the contributors of the Clang compiler and implying that ey is basically implementing ideas from Backus et al.