A Case for Imperative Reasoning

I've just finished watching a talk, the link is below, about operational semantics and the difficulty of specifying certain semantics in a purely declarative way. I really enjoyed the speaker, and I feel like I have a more complex view of the difference between imperative and declarative styles now. As someone who loves functional programming, it was interesting to see a reasonable case made about the challenges it faces in certain areas of specification. You have to watch a little bit into the talk to get the good parts, btw, as his opening statements about functional programming are not the interesting part.
The basic idea was that there are operational parts of an algorithm that may need to be specified for an implementation to be considered an instance of the algorithm (I'm taking a particular view of the notion of an algorithm, and this is discussed briefly in the talk) such as that a sort be in-place. I have no idea how we would state this directly in a functional language, except perhaps to build an functional description of an imperative process and some how ensure that it is carried out in a way the preserves the intended semantics.
The real reason I posted this is not just because it is interesting but because it is a rare thing to see an argument for imperative programming. I like this kind of thing because it adds a level of complexity and sophistication to the regular sort of arguments for or against one language/paradigm or another. I wonder though- he mentions that he uses intuitionistic logic in his current work, and as we all know the lambda calculus, and by extension Haskell, is an intuitionistic logic itself (through the Curry-Howard isomorphism) and programs are proofs of theorems in this logic. How this is related (if it indeed is related at all) I have no idea.

The link:
http://channel9.msdn.com/Blogs/Charles/C9-Conversations-Yuri-Gurevich-Abstraction-Algorithms-and-Logic