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

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.

• I guess, in the functional world, the denotational approach is quite natural. It is nicely compositional, unlike operational semantics (especially if small-step). I must confess I have never seen a Hoare logic for functional programs -- I suspect that one, if it exists, might be cumbersome since in pure FP there is no "update-the-state" construct like the assignment in imperative programming. – chi May 2 '17 at 23:02
• @chi Sure there are plenty of Hoare logics for FPs. The pioneering work was A Compositional Program Logic for Polymorphic Higher-Order Functions by Honda/Yoshida, this was extended in e.g. *An observationally complete program logic for imperative higher-order functions". It was extended in various ways. – Martin Berger May 3 '17 at 13:53
• @MartinBerger Ah, interesting. Thanks for the reference. – chi May 3 '17 at 14:21
• I find the references to FP distracting from the main point of the question. The difference between Hoare logic and denotational semantics is that the former is concerned with syntactically ascribing properties of programs (again, given syntactically) whereas the latter is concerned with associating programs with mathematical objects resembling their meaning. In other words, the two are very different. – Kai Sep 22 '17 at 14:02

$$\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.