What was the major breakthrough between Hoare-Floyd logic and Scott–Strachey semantics?
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.