The assignment statement \textt{x = x + 1} is a difference equation with its time index removed.
Program verification, from Hoare triples through weakest preconditions to TLA have been in part, a sixty-year effort to put this index back, but only for specification languages.

We present {\dpl}, a \emph{programming language} that never removes the index in the first place. Inside a loop, assignments take the form \texttt{v’ = f(v)} from the previous value to the next. At the end of each iteration, these updates commit.

This idea has never been tried for programming, although it abounds in specification languages.

Further, {\dpl} applies difference equations to arbitrary data types: arrays, sets, dictionaries, and pointer structures, making it a general-purpose language rather than a numerical-methods formalism.

{\dpl}’s syntactic discipline yields three benefits. First, textual order of updates is irrelevant in loops, which simplifies reasoning from beginners to experts. Second, loop invariant proofs reduce to reading the body as a relation and substituting—no backward reasoning, and frame conditions are carried by the notation rather than argued separately. Third, the same notation serves from introductory trace tables to relational Hoare proofs, with no change in vocabulary.

We show what it is like to work with {\dpl} with a variety of examples, sorting, graph search (DFS and BFS), Bellman-Ford, Relaxation methods, linked-list manipulation, and Schorr-Waite graph marking. We consider how this idea of committing loops could simplify other interesting application areas.