I'm reading through a commentary on Milner's "The use of machines to assist in rigorous proof" by Mike Gordon. In this paper, he explains how LCF was born from the ideas of denotational semantics by Dana Scott and Strachey.
It seems to me that Floyd-Hoare logic wasn't enough for developing LCF, but I'm not sure why this is the case. At the end, in Hoare logic we deal with program states that satisfy some precondition $P$ and that through a relation $r$ conform to some postcondition $Q$ and I can provide a formula for this. Wikipedia claims that denotational semantics:
is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages.
I'm familiar with some intuitions on how for instance recursion is modeled in this approach as a fixed point of some relation while in Hoare logic I didn't really remember dealing with recursion. Still both approaches seem to try to describe relations between inputs and outputs using mathematical relations.
So what is it that made a difference between Hoare logic and denotational semantics? Does denotational semantics manage better some complexities of programs? If so, please illustrate with an example.
Maybe the following quote of Milner referring to denotational semantics is interesting to guide your answer:
I could write down the syntax of a programming language in this logic and I could write the semantics in the logic.