What is the theoretical basis of imperative programming?

Functional programming has a theoretical basis in lambda calculus and combinatory logic. As someone involved with statistical computing, I find these concepts to be very useful for modeling.

Is there an equivalent mathematical basis of imperative programming, or did it simply grow out of practical hardware application in machine language and the subsequent development of FORTRAN?

In general, when mathematics is used to study some X, one first needs a model of X, and then develops a theory, a set of results about that model. I guess that theory may be said to be a "theoretical basis" for X. Now set X=computation. There are many models of computation, many involving "state". Each model has its own "theory" and it is sometimes possible to "translate" between models. I believe it's hard to say which model is more "basic"---they are simply designed with different goals in mind.

Turing machines were designed to define what is computable. So they make a good model if you care about whether there exists an algorithm for a certain problem. This model is sometimes abused to study the efficiency of algorithms or the hardness of problems, under the pretext that it's good enough, at least if you only care about polynomial/non-polynomial. The RAM model is closer to a real computer and therefore better if you want a precise analysis of an algorithm. To put lower bounds on the hardness of problems it is better to not use a model that resembles too much today's computers because you want to cover a wide range of possible computers, while still being more precise than just polynomial/non-polynomial. In this context, I saw for example the cell-probe model used.

If you care about correctness, then still other models are useful. Here you have operational semantics (which I'd say is the analogue of lambda calculus for statefull computations), axiomatic semantics (developed in 1969 by Hoare based on Floyd's inductive assertions from 1967, which are popularized by Knuth in The Art of Computer Programming, volume 1), and others.

To summarize, I think you are after models of computation. There are many such models, developed with various goals in minds, and many have state, so they correspond to imperative programming. If you want to know if something can be computed, then look at Turing machines. If you care about efficiency look at RAM models. If you care about correctness look at models that end in "semantics", such as operational semantics.

Finally, let me mention that there is a big book online only about Models of Computation by John Savage. It is mostly about efficiency. For the correctness part I recommend you start with the classic papers of Floyd (1967), Hoare (1969), Dijkstra (1975), and Plotkin (1981). They are all pretty cool.

The simplest theoretical model of an imperative program is the turing machine itself. It has both essential components of an imperative program: unbounded modifiable state and a state machine that operates on it.

You can also ground imperative programming into functional programming by considering programs as compositions of monadic operations that pass and return modified versions of the global state, as done in the Haskell programming language.

• Using monads to get imperative-like constructs in a purely functional language (such as Haskell) does not give you the full power of imperative programming. In particular, without truly mutable state (e.g. as in many languages with references), there are still many data structures whose efficient implementation in a purely functional language is unknown. Commented Aug 17, 2010 at 4:32
• @Joshua: Why do you think that state monads don't express the semantics of references? I'm at a loss to understand what the objection might be. Commented Aug 23, 2010 at 12:28
• A state monad is basically syntactic sugar for having a collection of functions that all accept an additional argument (state) and output an additional output (next state). But in a purely functional language you can't actually modify the state to get the next state, you still have to copy and reconstruct. I don't know if there are specific data structures where it is known that they cannot be implemented efficiently in a purely functional language, but there is certainly suggestive evidence (e.g. Pippenger. Pure vs. impure Lisp. 1997). Commented Aug 23, 2010 at 17:54
• One can capture the semantics of mutation with monads perfectly well -- see, e.g, the ST monad in Haskell. We're talking semantics here, not implementation.
– sclv
Commented Aug 23, 2010 at 20:44

In short, I would say that imperative programming evolved from machine language and programming practice. On the other hand, monads provide an appropriate semantic framework for describing the semantics of imperative programming language features. The paper Notions of computation and monads by Moggi established the formal foundations. Phil Wadler popularised the idea and contributed significantly to it being the key way of incorporating imperative features into the programming language Haskell. Recent work by Plotkin and Power Notions of Computation Determine Monads goes the other way stating that some, but not all, notions of (imperative) computation actually give a monad, meaning that in a very essential way monads correspond to imperative (and other) notions of computation.

• Monads can be used to cordon off imperative programming in a purely functional world, but I can't see the case for claiming that they form a theoretical basis for imperative programming analogous to the relationship between the lambda calculus and many functional languages. Monads don't model computation so much as they form an abstraction over classes of computation (e.g. pure computation vs. computation that involves IO, or computation that relies on a particular bundle of mutable state). Commented Aug 16, 2010 at 21:00
• Monads are a way to write clearer denotational semantic for effectful languages, so why not? Commented Nov 9, 2011 at 14:54

If you are looking for a rigorous mathematical treatment of an imperative programming language, Winskel's book "The Formal Semantics of Programming Languages" (1993) is an example.

In the book, he defines an imperative programming language called IMP and provides operational, denotational and axiomatic semantics of it.

I am coming to this question late, but it is a fascinating question. So, here are my views.

When I was an undergrad, we had a great Math professor, who used to give us lectures on history and development of mathematics. According to him, mathematics developed in waves of "expansion" and "consolidation". During an expansion phase, new ideas that were previously unknown were considered and investigated. Then, during a consolidation phase, the new theories were integrated into the existing body of knowledge. However, in the 20th century, he said, expansion and consolidation are going on in parallel.

Imperative programming is currently an expansion activity for mathematics. It was previously "unknown". (That may not be entirely true. Hoare tells us us that Euclid was doing something like imperative programming in his Geometry. But mathematics lost interest in it, for better or worse.) Mathematicians are still not interested in imperative programming. So much the loss for them. But I regard all of Computer Science as a branch of mathematics in an abstract sense. We are studying it, expanding mathematics in the process.

So, I wouldn't care particularly whether there is an a priori theoretical basis for imperative programming. If there isn't one, let us go and find it. What we know already tells us that imperative programming is fantastically deep and beautiful. Functional programming pales in comparison. But, we have a lot of work to do to bring all this theory out to people.

• "Functional programming pales in comparison". Now if only I could get you and Bob Harper into a fighting arena. You'd swing a big block of commands and he'd try to cast a closure upon you. (P.S.: very good answer, I upvoted it.) Commented Feb 25, 2012 at 6:52
• Well, he sort of avoids me. I don't know if that means anything :-) Commented Feb 25, 2012 at 22:39

Functional programming has a clear basis in mathematics because functional programming languages evolved in parallel with the relevant math and their designers typically held the math in high regard. The strong and straightforward relationship is a self-fulfilling prophecy.

Imperative programming has a significantly messier history that's tied much more closely to business and engineering problems and was historically much more concerned with the performance of compilers and the code that they generate than with respecting mathematical formalisms.

Many people have attempted to explain imperative programming in (traditionally) functional terms. This may be the closest we can get to what you're looking for, but these attempts are invariably awkward, tedious, forensic. I'm pretty sure I would rather tear my eyes out of my face than read a progress/preservation proof for the CLR.

Usually if you get towards the end of a decent pl textbook (e.g. Pierce's Types and Programming Languages), you'll start to see formal modeling of imperative language features. This may be interesting to you.

An Axiomatic Basis for Computer Programming by C. A. R. HOARE

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantages, both theoretical and practical, may follow from a pursuance of these topics.

I second what Alexandre said, that the Turing machine provided the original theoretical basis for imperative programming. To the extent that the organization of imperative programming languages reflect the machine architecture, I think that the work of John Von Neumann would also be a key part of the their theoretical foundations.

Is there an equivalent mathematical basis of imperative programming, or did it simply grow out of practical hardware application in machine language and the subsequent development of FORTRAN?

If you mean "basis" in the historical sense, I think that there is no "equivalent mathematical basis". However, even though imperative programming grew out of practical concerns, there are several ways of comprehensively characterizing the meaning of imperative programming in ways that you might find "useful for modeling", such as Hoare logic.

• did you really mean to make this community wiki ? Commented Aug 16, 2010 at 22:08
• Yes, I did mean to make it community wiki. Commented Aug 16, 2010 at 22:39

the posts that mention hoare logic and separation logic are the correct ones on this matter. Hoare logic lets you state properties of the entire heap configuration of a program, and separation logic is the more modern relative which lets you use a "separating conjunction" that lets you state as pre and post conditions to a segment of code what properties hold for the part of the heap that the program segment will manipulate while quantifying over the rest of the heap.

The answer regarding monads is not strictly accurate, because in haskell a monad is used merely because it is an abstraction that enables the encoding of order of evaluation constraints and explicit tracking of the "might use IO" property.

It is worth pointing out both that hoare/separation logic can be view as monads, and that there are a number of contemporary projects such as the ynot project at harvard which are exploring these topics.

research in separation logic is an ongoing and active field.

• It seems to me an error to confuse the fact that Haskell uses a notion of monads (and a Monad typeclass) with the more general approach, as put forward by e.g., Moggi, that uses monads to structure an account of categorical semantics. The adoption of monads as a tool to structure programming shouldn't blind us to the use of categorical semantics as a tool to structure reasoning about programming.
– sclv
Commented Aug 25, 2010 at 0:25
• very good clarification, though I do believe that a whole slew of folks have used monads a la haskell to explore semantics via monad transformers. In particular, the differing semantics for operations that arise from different compositions of said transformers (eg for state/mutability, continuations, nondeterminism etc) Commented Aug 25, 2010 at 4:57

I am coming to this question even later, but I am equally fascinated by it.

Why the theory of imperative programming is considered less settled than that of functional programming evades me. It probably started to get serious with Scott and de Bakker in 1969 with their analysis of the meaning of recursion in a simple imperative language [1]. When the imperative language gains features, the story gets a bit messier but that is just the price to pay for being closer to the metal. To name one of the more comprehensive efforts, in 1980, de Bakker, de Bruin, and Zucker wrote a monograph on the subject [2]. Others were mentioned above. These references of course pre-date separation logic but [2] nevertheless tackles arrays and mutually recursive procedures.

[1]: unpublished in 1969 but appeared as Jaco W. de Bakker and Dana S. Scott. A Theory of Programs, pages 1-30. In Klop et al. J. W. de Bakker, 25 jaar semantiek. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Mathematical theory of program correctness. Prentice Hall 1980.

• Clearly imperative programming is extremely well understood. I think what people mean when they say it's less settled is that structurally, imperative programming is richer than pure functional programming, and a lot less mathematical structure has been discovered that crops up in this or that form of imperative programming. For example, certain kinds of imperative programs can be reasoned about nicely using separation logic. This is probably to do with forms of sharing. Maybe these kinds of programs have a nice, abstract mathematical characterisation? Commented Feb 28, 2012 at 15:36
• Personally, I mean the theory of modularity in imperative languages is very unclear. We know what modularity means for functional languages: relational parametricity. For imperative languages, there are many information-hiding idioms that (a) clearly work, but (b) for which we lack good proof techniques. There are tantalizing hints that there is a deep theory here: for instance, when I do modular proofs of sequential imperative programs, I end up needing techniques from concurrency. Informally, aliasing is like concurrency, but I don't really know how to formalize that idea... Commented Feb 29, 2012 at 8:55
• @Kai. Welcome to the thread! It has been a long time since I looked at the de Bakker work, but I think the basic problem is that the approach did not scale up. For a quick summary of the progress on imperative programming since then see my post in the "What constitutes denotational semantics?" thread link. Commented Mar 1, 2012 at 11:44
• @NeelKrishnaswami. I would love to see those proofs. Are they on your web page? Aliasing is like concurrency in that they both involve sophisticated sharing and interleaving. In concurrency, you abstract away the interleaving and assume nondeterminism (which is good). In aliasing, you force yourself to deal with the interleaving. Games semantics is an excellent example of this forced interleaving, which is the reason I don't like it. Commented Mar 1, 2012 at 12:24

Shortly after you asked your question, Mark Bender of McMaster University released a thesis: Assignment Calculus: A Pure Imperative Reasoning Language (2010 Sep 8). This thesis describes a simple, imperative language corresponding to lambda calculus.

Assignment calculus consists of only four basic constructs, assignment X:=t, sequence t;u, procedure formation ¡t and procedure invocation !t. Three interpretations are given for AC: an operational semantics, a denotational semantics, and a term-rewriting system. The three are shown to be equivalent.

Mark Bender's thesis goes on to explore variants extended with lazy evaluation, backtracking, procedure composition. This is similar to exploration of lambda calculus by use of small extensions.

Overall, the thesis provides a relatively direct answer to the OP question.

• pdf link is broken Commented May 14, 2017 at 17:36