A Discipline of Programming

It's clear that Dijkstra was a great thinker who had bad tools available to him. It's a wondrous thing to imagine what he'd get done with a proof assistant in his tool-belt. This book is... dated. It has lots of good ideas at the beginning and at the end, but the middle is a bunch of EXTREMELY IMPERATIVE SOLUTIONS to problems, with long digressions on features of his make-believe programming language's features.