Reasoned Programming by Krysia Broda, Susan Eisenbach, Hessam Khoshnevisan, and Steve Vickers.
From the preface:
Can we ever be sure that our computer programs will work reliably? One approach to this problem is to attempt a mathematical proof of reliability, and this has led to the idea of Formal Methods: if you have a formal, logical specification of the properties meant by `working reliably’, then perhaps you can give a formal mathematical proof that the program (presented as a formal text) satisfies them.
Of course, this is by no means trivial. Before we can even get started on a formal proof we must turn the informal ideas intended by `working reliably’ into a formal specification, and we also need a formal account of what it means to say that a program satisfies a specification (this amounts to a semantics of the programming language, an account of the meaning of programs). None the less, Formal Methods are now routinely practised by a number of software producers.
However, a tremendous overhead derives from the stress on formality, that is to say, working by the manipulation of symbolic forms. A formal mathematical proof is a very different beast from the kind of proof that you will see in mathematical text books. It includes the minutest possible detail, both in proof steps and in background assumptions, and is not for human consumption &emdash; sophisticated software support tools are needed to handle it. For this reason, Formal Methods are often considered justifiable only in `safety critical’ systems, for which reliability is an overriding priority.
The aim of this book is to present informal formal methods, showing the benefits of the approach even without strict formality: although we use logic as a notation for the specifications, we rely on informal semantics &emdash; a programmer’s ordinary intuitions about what small, linear stretches of code actually do &emdash; and we use proofs to the level of rigour of ordinary mathematics.
A bit dated (1994) and teaches Miranda, a functional programming language and uses it to reason about imperative programming.
Even thinking about a “specification” isn’t universally admired these days but the author’s cover that point when they say:
This `precise account of the users’ needs and wants’ is called a specification, and the crucial point to understand is that it is expressing something quite different from the code, that is, the users’ interests instead of the computer’s. If the specification and code end up saying the same thing in different ways &emdash; and this can easily happen if you think too much from the computer’s point of view when you specify &emdash; then doing both of them is largely a waste of time. (emphasis added, Chapter 1, Section 1.3)
That’s blunt enough. 😉
You can pick up Miranda, homesite or translate the examples into a more recent functional language, Clojure comes to mind.
I first saw this in a tweet by Computer Science.