7
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – chi May 2 '17 at 23:02
  • 3
    $\begingroup$ @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. $\endgroup$ – Martin Berger May 3 '17 at 13:53
  • $\begingroup$ @MartinBerger Ah, interesting. Thanks for the reference. $\endgroup$ – chi May 3 '17 at 14:21
  • $\begingroup$ 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. $\endgroup$ – Kai Sep 22 '17 at 14:02
9
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.