Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Refinement Calculus

Programming from Specifications

• rating: 1

I have a dead tree version of this. While it's not on archive.org, there are .ps files on the author's website.

Not sure if I'm a fan of parts of this calculus. It's interesting to know about, for sure. The author wrote a paper previous to this (I believe its the one about violating the law of the excluded miracle), where this calculus is introduced. One of the highlighted features of it is that it is a unified formalism, it contains both the specification relation and the program. It's all one. The book emphasizes this too. Is that a good thing though? Maybe. I mean it is, but it feels like sometimes it makes the formalism more awkward than it needs to be.

a Practical Theory of Programming

• rating: TODO

.

Refinement Calculus: A Systematic Introduction

• rating: TODO

Extends the refinement calculus to allow it to handle game semantics.

Can Programming Be Liberated from the von Neumann Style?

• rating: classic

Contains the assertion that "von Neumann languages lack useful mathematical properties".

Since this paper was written, there have been two schools of thought, based on the reaction to this assertion.

One school agrees with the assertion and has persued what Wikipedia calls "function-level programming" which is sometimes also called "point-free programming" or "calculation of programs", or more loosely "equational reasoning", and of which concatenative languages and recursion schemes are followers to an extreme degree.

The other school agrees with the assertion but accepts the reality that von Neumann languages are entrenched and, often, are the languages with which the highest performance can be achieved, so has, in some sense, shouted "damn the torpedoes" and has wrestled with turning von Neumann programming from an art into a science despite its lack of useful mathematical properties. This school has given us "separation logic" among other things.

Algorithmics

• rating: 3

Motivates a lot of the "calculational style" of developing programs. Point-free programming, concatenative languages, and recursion schemes are all related.

Laws of Programming

• rating: 3

This applies the ideas of "calculational style" to imperative, rather than functional, programs. In the process it gives a mini-overview of denotational semantics. Since specifications and programs are written in the same notation, this leads into what is often called "program refinement".

Algebraic Identities for Program Calculation

• rating: 3

Bird offers a good definition of "calculate" in this context:

To calculate a program means to derive it from a suitable specification by a process of equational reasoning.

The specification statement

• rating: classic

.

Correctness Preserving Program Refinements

• rating: 0

.

Refinement Calculus

• rating: 3

.

The Retrenchment Homepage

• rating: 1

.