Comment by mcguire | Hacker News Reader

Comment by mcguire | Hacker News Reader

Coming from the land of Dijkstra (UTAustin, by the way), pre- and post-conditions were how I learned to think about programs. Things like denotational semantics and what-not seem odd and somehow magical to me, even after a lot of experience with languages like Haskell that incorporate that kind of thinking.

I'm not going to get this right because I haven't even thought it out to my own satisfaction, but the fundamental difference seems to me to be that the those things treat a program as a mathematical object in itself, which is one of the reasons they focus on functional languages and immutability.

Floyd-Hoare treats the program as a text; it assigns states to the spaces between statements. As a result, it's pretty darn happy with imperative programming, although it has its own limits.

(As an aside (Did I mention that I once worked in the same building as Dijkstra, although I never took a class from him.), I find it very amusing that the article has the sentence "There are rules for concurrency, procedures, jumps, and pointers." although neither it nor the linked "Branch" article actually describe Knuth's revelation of Hoare's axioms for goto.)

Coming from the land of Dijkstra (the Netherlands), I was taught about this in college and it was very cool to use this to prove that post-conditions of a function are actually true (although finding good loop invariants was sometimes a bit annoying.

Denotational semantics are horrible in my opinion, but I really like operational semantics (especially structural operational semantics and natural semantics), they still consider a program as a single mathematical object, but like Hoare logic it also tracks the state before and after each statement. It's really easy to work to with (just apply rules), but sadly it's a bit less powerful than Hoare logic, as you can't infer things that hold in general, you can only reason about specific begin states.

Your background immediately reminded me of Betrand Meyer and Design by Contract[1]. I wonder how much of Hoare's work influenced Meyer.

Do you care to opine? :-)

1 - http://www.artima.com/intv/contracts.html

I don't know much about Meyer's history and the history of Design by Contract, but I'm going to go out on a limb and say, "quite a bit." The major difference that I can see, with my limited experience, is that DbC seems to be focused on the boundaries between functions and is more closely related to assertions (which are probably also related to Hoare).

Huh, funny, I have completely the opposite standpoint.

I see the point of semantics as capturing what programs mean. Denotational semantics does this in the most direct way, by giving me a mapping from programs to some abstract domain I can reason about and manipulate. It's literally a function from program to meaning.

It exposes a simple and natural model of my program—or, in the case of imperative programming, perhaps not so simple. As a facetious example, what should the program "1 + 1" mean? Adding two numbers seems like the most natural choice. But this can actually scale up quite far, producing simple models even for complex behaviors[1] as long as the language and libraries are designed with some taste.

Having simple denotational semantics captures exactly what it means for a language to be truly declarative, where we can think about what the program means and not how it happens to be executed.

Operational semantics is the next most direct option. It captures the meaning of a program by how it gets executed. Not quite declarative, but still reasonably easy to follow.

Axiomatic semantics, on the other hand, are really indirect. I mean, yes, I can see how you can capture a program's whole meaning by how preconditions are transformed throughout, but that's pretty far from what I think a program means. It's certainly useful and good for answering some very specific questions about a program's behavior, but it feels like a really unsatisfying answer to the broader question of semantics: what does it all mean?

[1]: A great example of how it scales to domains that are normally incredibly difficult to work with is functional reactive programming (FRP), which has a simple denotational model for working with time-varying values (ie reactive code). Unfortunately, as is too-often the case with nice abstractions, it has been hard to implement in general without compromises—but the nice thing is that we can know exactly what the compromises are by comparing the more complicated semantics of those libraries with the simple ones that we'd really like.

Reply on news.ycombinator.com