An Axiomatic Basis for Computer Programming (1969) [pdf] | Hacker News Reader

An Axiomatic Basis for Computer Programming (1969) [pdf]

cs.toronto.edu

29 pointstjalfi16 comments

Thanks for posting this--I'm getting back into studying the formal semantics of programming languages. Questions for those working in this area:

According to Pierce's Types and Programming Languages, axiomatic semantics of the type that Hoare pioneered are not found as useful today as operational semantics. Is that (still) true?

Are the major approaches (operational, denotational, axiomatic) pretty much solidified now, or are there significant new efforts at finding better overall formalizing frameworks?

There is only one formalising framework, it is called math. The rest is just noise.

When trying to make a better framework for formalising computer programs, just make a better framework for formalising math first.

You can't make a better framework for formalising math, because, as you've yourself said, "there is only one formalising framework", and it's math itself. Cue the problems with self-application and Goedel's tricks :)

Yeah, in a way you are right.

Ok, let me put it this way: Math is not formal. But, formality has its advantages, so what I would like to see is a framework that, while being formal, still allows formulating ideas just as a mathematician would. Kind of like envisioned here: https://www.practal.com

Math has many formalisms. Some more useful than others, in certain contexts. All restricted by the norms of communication that they are written in.

So, yes, there are some math formalities for processes. No, they probably don't help in finding new processes as much as you'd think. Despite being quite good at understanding existing processes through formal exploration.

Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done.

The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.

VerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls.

[1]https://vst.cs.princeton.edu/veric/

[2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.

No goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one:

      { pre(L) }  S;  { P }
    ------------------------
    { pre(L) }  L: S;  { P }
    
    
    { pre(L) }  goto L;  { false }

You just have to use the same precondition pre(L) for every mention of the label L.

https://softwarefoundations.cis.upenn.edu/

Hoare's thoughts on the 40th anniversary: https://cacm.acm.org/magazines/2009/10/42360-retrospective-a...

Discussed (barely) at the time:

Retrospective: An Axiomatic Basis for Computer Programming - https://news.ycombinator.com/item?id=905176 - Oct 2009 (1 comment)

Also read Robert Floyd's paper Assigning Meanings to Programs.

After getting the gist of the above, reading Bertrand Meyer's Design by Contract and Applying Design by Contract will clarify on how to apply the ideas to "real" systems.

A gem of readability and clarity.

How does one read it? I simply can't read it, only see the first page

Did you try more than one viewer? It renders fine in Evince and in Vivaldi here. The 'bodies' of the pages are not regular text but images over that background gradient, by the way.

Works for me but found this less unusual pdf: http://www.cs.toronto.edu/~chechik/courses05/csc410/readings...

(submitter)

Thanks, I have asked dang to update the link.

Reply on news.ycombinator.com