What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?

Question

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.

Question

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.

Answer 1

I don't know why people didn't develop Hoare logics for lambda-calculi earlier. The first work to get this right was Honda et al's

A Compositional Program Logic for Polymorphic Higher-Order Functions

There were some earlier attempts before this, but they didn't quite nail the problem, for example: how do you denote the value of a functional program? What piece of syntax corresponds to the function space constructor? There are a couple of little things that need to be gotten right.

Let me speculate: maybe the main issue was that Hoare logic was typically concerned with stateful computation. If you combine state and higher-order functions, you immediately have to deal with aliasing, e.g. programs like

$$\lambda x^{\mathsf{Ref(Nat)}}.\lambda y^{\mathsf{Ref(Nat)}}.(x := !x+1; y := !y+1),$$ as well as local store and recursion through the store. These were only solved in the early 2000s in works like An observationally complete program logic for imperative higher-order functions (recursion through the store); A logical analysis of aliasing in imperative higher-order functions (aliasing), Logical Reasoning for Higher-Order Functions with Local State (full local store). At the same time Separation logic tackled the aliasing problem form a different angle.

This work has been implemented in Coq by A. Charguéraud in his work, and that is also used in the Javascript semantics now.