Pure Imperative programming language

Status: on hold, stale; 2006 (supersedes any conflicting remarks left on this page; see the home page for definitions)

Here are some ideas for a "Pure Imperative" programming language that is a precursor to the one in my vision for a computing platform.  I'm not sure if I still like all the ideas here.

1. Most widely used imperative programming languages offer a "chaotic heap", or one consisting of an arbitrary number of objects, any of which can hold a reference to any other.  This is convenient for the programmer but makes code more difficult to understand and maintain due to aliasing.  On the other hand, the Pure Imperative heap consists of a tree of objects.  The language provides no support for references per se, but they are easy for the programmer to emulate using a sequence of steps up and down the tree, some of which involve array indexes.  For example, a graph might contain an array of vertices and an array of edges; the endpoints of an edge are essentially given as indices into the array of vertices.  In practice, the compiler will often be able to optimize such emulated references into plain pointers.
2. Pure Imperative objects are passed by value, which eliminates aliasing and thereby makes it easier to reason about a program's behavior.  In source code, it is trivial to deep-copy an object.  That is to say, the operation has the semantics of deep-copying, but it is much faster.  Pure Imperative has a clever heap implementation called the "zip-unzip heap" that provides reads, writes, and deep copies all in amortized constant time (not sure of this); it is based on ideas from the version-control system git.  Pass-by-reference is emulated by copying in and then copying out.  Often the compiler will be able to optimize out the copies of arguments when routines are called and then return.
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.
4. Pure Imperative supports very flexible and precise data definition.  It offers all the types one would find in, for example, MySQL; its emulated references deserve to be compared to foreign keys.  Programmers can place invariants on data and prove that the invariants are preserved.  Pure Imperative will support union types with a pattern-matching switch statement like Cyclone's.  Unlike C, it allows a structure to contain a member of its own type.  The combination of these two makes it great for abstract syntax trees.