<p>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.</p>

<p>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.</p>

CC BY-SA 2.5
2010-08-23T12:28:46.830Z
@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.
Charles Stewart
CC BY-SA 2.5
2010-08-23T17:54:08.277Z
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).
Joshua Grochow
CC BY-SA 2.5
2010-08-23T20:44:51.203Z
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
CC BY-SA 2.5
2010-08-17T04:32:19.150Z
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.
Joshua Grochow
CC BY-SA 2.5
2010-08-16T21:13:47.323Z
2010-08-16T21:13:47.323Z
Alexandre Passos
<p>In short, I would say that imperative programming evolved from machine language and programming practice. On the other hand, <a href="http://en.wikipedia.org/wiki/Monad_%28functional_programming%29">monads</a> provide an appropriate semantic framework for describing the semantics of imperative programming language features. The paper   <a href="http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf"><em>Notions of computation and monads</em></a> 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 <a href="http://hdl.handle.net/1842/196"><em>Notions of Computation Determine Monads</em></a> 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.</p>

CC BY-SA 3.0
2011-11-09T14:54:00.330Z
Monads are a way to write clearer denotational semantic for effectful languages, so why not?
nponeccop
CC BY-SA 2.5
2010-08-16T21:00:15.727Z
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).
blucz
CC BY-SA 2.5
2010-08-16T20:39:06.183Z
2010-08-16T20:39:06.183Z
Dave Clarke
<p>I am coming to this question late, but it is a fascinating question.  So, here are my views.</p>

<p>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.</p>

<p>Imperative programming is currently an expansion activity for mathematics.  It was previously "unknown".  (That may not be entirely true.  <a href="http://www.computingatschool.org.uk/index.php?id=hoare">Hoare tells us</a> 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.</p>

<p>So, I wouldn't care particularly whether there is an <i>a priori</i> 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.</p>

CC BY-SA 3.0
2012-02-25T06:52:08.953Z
"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.)
Andrej Bauer
CC BY-SA 3.0
2012-02-25T22:39:52.257Z
Well, he sort of avoids me.  I don't know if that means anything :-)
Uday Reddy
CC BY-SA 3.0
2012-02-24T00:16:20.023Z
2012-02-25T22:45:49.643Z
2012-02-25T22:45:49.643Z
Uday Reddy
<p><code>An Axiomatic Basis for Computer Programming</code> by C. A. R. HOARE</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&amp;rep=rep1&amp;type=pdf">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&amp;rep=rep1&amp;type=pdf</a></p>

CC BY-SA 2.5
2010-08-24T16:58:50.113Z
2010-08-24T16:58:50.113Z
Vag
<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 2.5
2010-08-16T21:11:33.283Z
2010-08-16T21:11:33.283Z
blucz
<p>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.</p>

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

CC BY-SA 2.5
2010-08-17T10:47:26.487Z
2010-08-17T10:47:26.487Z
yhirai
<p>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 <a href="http://en.wikipedia.org/wiki/Von_Neumann_architecture">John Von Neumann</a> would also be a key part of the their theoretical foundations.</p>

CC BY-SA 2.5
2010-08-18T02:42:13.423Z
2010-08-18T02:42:13.423Z
Kurt
<blockquote>
  <p>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?</p>
</blockquote>

<p>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 <a href="http://en.wikipedia.org/wiki/Hoare_logic" rel="noreferrer">Hoare logic</a>.</p>

CC BY-SA 2.5
2010-08-16T22:08:46.800Z
did you really mean to make this community wiki ?
Suresh Venkat
CC BY-SA 2.5
2010-08-16T22:39:46.150Z
Yes, I did mean to make it community wiki.
jbapple
CC BY-SA 2.5
2010-08-16T22:05:38.467Z
2010-08-16T22:05:38.467Z
jbapple
<p>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. </p>

<p>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. </p>

<p>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 <a href="http://ynot.cs.harvard.edu/" rel="noreferrer">the ynot project</a> at harvard which are exploring these topics.</p>

<p>research in separation logic is an ongoing and active field.</p>

CC BY-SA 2.5
2010-08-25T00:25:11.157Z
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
CC BY-SA 2.5
2010-08-25T04:57:10.757Z
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)
Carter Tazio Schonwald
CC BY-SA 2.5
2010-08-24T20:19:16.720Z
2010-08-25T04:57:22.880Z
2010-08-25T04:57:22.880Z
Carter Tazio Schonwald
<p>I am coming to this question even later, but I am equally fascinated by it.</p>

<p>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.</p>

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

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

CC BY-SA 3.0
2012-02-28T15:36:17.260Z
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?
Martin Berger
CC BY-SA 3.0
2012-02-29T08:55:51.327Z
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...
Neel Krishnaswami
CC BY-SA 3.0
2012-03-01T11:44:47.907Z
@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](http://cstheory.stackexchange.com/a/10451/8519).
Uday Reddy
CC BY-SA 3.0
2012-03-01T12:24:56.140Z
@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.
Uday Reddy
CC BY-SA 3.0
2012-02-28T10:50:49.727Z
2012-02-28T10:50:49.727Z
Kai
<p>Shortly after you asked your question, Mark Bender of McMaster University released a thesis: <a href="https://www.semanticscholar.org/paper/Assignment-Calculus-A-Pure-Imperative-Reasoning-La-Bender-Zucker/c168e5fc64a6de9953a9a8985ee17b0ac291e299" rel="nofollow noreferrer">Assignment Calculus: A Pure Imperative Reasoning Language</a> (2010 Sep 8). This thesis describes a simple, imperative language corresponding to lambda calculus.</p>

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

<p>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. </p>

<p>Overall, the thesis provides a relatively direct answer to the OP question.</p>

CC BY-SA 3.0
2017-05-14T17:36:14.150Z
pdf link is broken
Quinn Wilson
CC BY-SA 3.0
2014-05-25T15:27:47.953Z
2017-06-26T18:35:50.620Z
2017-06-26T18:35:50.620Z
dmbarbour
<p>In general, when mathematics is used to study some <em>X</em>, one first needs a model of <em>X</em>, 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 <em>X</em>. Now set X=computation. There are <em>many</em> 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.</p>

<p>Turing machines were designed to define what is <em>computable</em>. 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 <em>efficiency</em> of algorithms or the <em>hardness</em> 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 <em>not</em> 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.</p>

<p>If you care about <em>correctness</em>, 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 <em>The Art of Computer Programming</em>, volume 1), and others.</p>

<p>To summarize, I <em>think</em> 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.</p>

<p>Finally, let me mention that there is a big book online only about <a href="http://www.cs.brown.edu/~jes/book/pdfs/ModelsOfComputation.pdf">Models of Computation</a> by John Savage. It is mostly about efficiency. For the correctness part I recommend you start with the classic papers of <a href="http://scholar.google.com/scholar?cluster=2215741797543540501">Floyd (1967)</a>, <a href="http://scholar.google.com/scholar?cluster=4957422039574646466">Hoare (1969)</a>, <a href="http://scholar.google.com/scholar?cluster=2051254789593517635">Dijkstra (1975)</a>, and <a href="http://scholar.google.com/scholar?cluster=17160779484259521873">Plotkin (1981)</a>. They are all pretty cool.</p>

CC BY-SA 4.0
2021-08-19T11:46:50.150Z
For future readers, Models of Computation seems to have moved to https://cs.brown.edu/people/jsavage/book/pdfs/ModelsOfComputation.pdf
Higemaru
CC BY-SA 2.5
2010-08-23T20:47:34.770Z
I think Operational Semantics is indeed what the poster is looking for. A bit more info on wikipedia: http://en.wikipedia.org/wiki/Operational_semantics
sclv
CC BY-SA 2.5
2010-08-18T13:07:11.397Z
2010-08-18T13:28:46.200Z
2010-08-18T13:28:46.200Z
Radu GRIGore
<p>Functional programming has a theoretical basis in <a href="http://en.wikipedia.org/wiki/Lambda_calculus">lambda calculus</a> and <a href="http://en.wikipedia.org/wiki/Combinatory_logic">combinatory logic</a>.  As someone involved with statistical computing, I find these concepts to be very useful for modeling.</p>

<p>Is there an equivalent mathematical basis of <a href="http://en.wikipedia.org/wiki/Imperative_programming">imperative programming</a>, or did it simply grow out of practical hardware application in machine language and the subsequent development of <a href="http://en.wikipedia.org/wiki/FORTRAN">FORTRAN</a>?</p>

<imperative-programming><pl.programming-languages>
What is the theoretical basis of imperative programming?
Shane
# What is the theoretical basis of imperative programming?

(Asked by: username_0 on 2010-08-16)

Functional programming has a theoretical basis in [lambda calculus](http://en.wikipedia.org/wiki/Lambda_calculus) and [combinatory logic](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Imperative_programming), or did it simply grow out of practical hardware application in machine language and the subsequent development of [FORTRAN](http://en.wikipedia.org/wiki/FORTRAN)?

**Tags:** imperative-programming, pl.programming-languages

---

## 12 answers

### Answer by username_21 on 2010-08-18. Score: 28 | Accepted answer

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](http://www.cs.brown.edu/~jes/book/pdfs/ModelsOfComputation.pdf) by John Savage. It is mostly about efficiency. For the correctness part I recommend you start with the classic papers of [Floyd (1967)](http://scholar.google.com/scholar?cluster=2215741797543540501), [Hoare (1969)](http://scholar.google.com/scholar?cluster=4957422039574646466), [Dijkstra (1975)](http://scholar.google.com/scholar?cluster=2051254789593517635), and [Plotkin (1981)](http://scholar.google.com/scholar?cluster=17160779484259521873). They are all pretty cool.

> **Comments:**
> **username_4**: I think Operational Semantics is indeed what the poster is looking for. A bit more info on wikipedia: http://en.wikipedia.org/wiki/Operational_semantics  
> **username_22**: For future readers, Models of Computation seems to have moved to https://cs.brown.edu/people/jsavage/book/pdfs/ModelsOfComputation.pdf  

---

### Answer by username_1 on 2010-08-16. Score: 22

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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: @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.  
> **username_3**: 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).  
> **username_4**: 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.  

---

### Answer by username_5 on 2010-08-16. Score: 20

In short, I would say that imperative programming evolved from machine language and programming practice. On the other hand, [monads](http://en.wikipedia.org/wiki/Monad_%28functional_programming%29) provide an appropriate semantic framework for describing the semantics of imperative programming language features. The paper [*Notions of computation and monads*](http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf) 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*](http://hdl.handle.net/1842/196) 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.

> **Comments:**
> **username_7**: 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).  
> **username_6**: Monads are a way to write clearer denotational semantic for effectful languages, so why not?  

---

### Answer by username_11 on 2010-08-17. Score: 15

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.


---

### Answer by username_8 on 2012-02-24. Score: 14

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](http://www.computingatschool.org.uk/index.php?id=hoare) 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.

> **Comments:**
> **username_9**: "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.)  
> **username_8**: Well, he sort of avoids me.  I don't know if that means anything :-)  

---

### Answer by username_10 on 2010-08-24. Score: 11

`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.

<http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf>


---

### Answer by username_7 on 2010-08-16. Score: 11

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.


---

### Answer by username_12 on 2010-08-18. Score: 8

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](http://en.wikipedia.org/wiki/Von_Neumann_architecture) would also be a key part of the their theoretical foundations.


---

### Answer by username_13 on 2010-08-16. Score: 7

> 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](http://en.wikipedia.org/wiki/Hoare_logic).

> **Comments:**
> **username_14**: did you really mean to make this community wiki ?  
> **username_13**: Yes, I did mean to make it community wiki.  

---

### Answer by username_15 on 2010-08-24. Score: 7

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](http://ynot.cs.harvard.edu/) at harvard which are exploring these topics.

research in separation logic is an ongoing and active field.

> **Comments:**
> **username_4**: 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.  
> **username_15**: 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)  

---

### Answer by username_16 on 2012-02-28. Score: 5

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.

> **Comments:**
> **username_17**: 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?  
> **username_18**: 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...  
> **username_8**: @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](http://cstheory.stackexchange.com/a/10451/8519).  
> **username_8**: @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.  

---

### Answer by username_19 on 2014-05-25. Score: 4

Shortly after you asked your question, Mark Bender of McMaster University released a thesis: [Assignment Calculus: A Pure Imperative Reasoning Language](https://www.semanticscholar.org/paper/Assignment-Calculus-A-Pure-Imperative-Reasoning-La-Bender-Zucker/c168e5fc64a6de9953a9a8985ee17b0ac291e299) (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.

> **Comments:**
> **username_20**: pdf link is broken  

---

