# Pure Imperative programming language

3. Pure Imperative code is imperative (deals with mutable variables), but the side effects of each routine are isolated to those arguments that will be copied out; in that sense, the language is pure.  Both functional and imperative programming patterns can be expressed naturally in Pure Imperative.  A mechanically checked mathematical proof system is provided so that programmers can prove that their imperative code computes a mathematical function whose statement need not be computationally effective.  For example, a programmer can write an imperative implementation of Dijkstra's algorithm and then prove that it computes the minimum of $\sum_{i=0}{n-1} d(A_i,A_{i+1})$ over all sequences of vertices $A_0$, \dots, $A_n$ such that $A_i$ is adjacent to $A_{i+1}$ for each $i$.  "For all" or "over all" is the most common computationally ineffective construct; it is either prohibitively slow or impossible to compute exhaustively.