Dijkstra was very much interested in keeping programs cognitively manageable. I can’t imagine he’d object to a program being readable. He’d see it as mathematical elegance.

That said, for readers untrained in the predicate calculus, his work can be impenetrable. Fortunately anyone smart enough to program is smart enough to learn the predicate calculus. I use it regularly in real work. I don’t bother constructing fully formally correct programs, but I use invariants to write all but the most trivial loops.