With discipline and the proper application of the predicate calculus it's no harder to write provably correct imperative programs than it is functional ones. I'm most familiar with the work of Dijkstra and Scholten, but I'm certain that Hoare, Lamport, and many others have made great use of the technique or very similar ones. Note that this method is not proving the correctness of arbitrary programs, it is deriving programs that must be correct because of the way in which they were written. The introductory paper[1] is readable and short and I recommend anyone interested read it.

That said, since in this case one is working with predicate transformers, which are mathematical objects, perhaps one can support the claim that it's just applying functional methods to imperative programming. I'm not so sure, but in the end it's not very important to me either way. I just like knowing that I have strategies for writing good programs be they functional or imperative.

This does make me doubt the practical usefulness of the Turing machine model for the professional software engineer though. I'm not aware of any technique that derives nontrivial correct programs using Turing machines. While the most formal predicate transformer based approaches are relatively rarely used and only for the trickiest problems, anyone who is familiar with both will recognize that properly applied TDD is extremely similar, so much so that I consider it a sufficiently rigorous informal approximation for the vast majority of practical cases.

[1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD472...