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.
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.
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 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.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf
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.
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.
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.
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, sequencet;u, procedure formation¡tand 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.
