Traveling through time is a pretty common science fiction trope, so much so that there are differing theories as to what happens if you go back in time and affect the past. While time travel has made for some entertaining movies and books, there’s been little success in the real world. The 2005 time traveler convention hosted at the MIT volleyball courts drew zero time travelers.

Now there’s a toy programming language called Mariposa that claims to implement time travel as part of its feature set. Toy languages are created as a way to play around with a novel or odd feature, like variable assignment outside of the normal order of execution—more colloquially, time travel.

Time travel in programming terms generally means stepping forwards and backwards through code or retrieving previous states, not manipulating real, four-dimensional space time. We’re not quite in that future yet (or are we?). But computer science has long sought to reason about time in electronic systems, thanks to a consistent interest in concurrency and real-time messaging.

In this article, I’ll take a look at the time travel capabilities of Mariposa (and other languages) and share the history and future of other programming paradigms that use temporal logic.

Mariposa allows you to manipulate the order of execution by assigning an instant to a variable, then setting the context of that instance. Here’s a basic example, taken from the Mariposa readme:

x = 1
t = now()
print(x)
at t:
  x = 2

According to the normal order of operations, this code should print “1”. But because t is assigned to the instance in the second line, any modifications specified within an at t: block are applied immediately, and this code prints “2”. The language limits traveling to the same instance twice and allows reading and writing values in parent frames.

With some chaining and setting t = $(now()) within at t: blocks—that is, changing the current instance from within a time traveling context—you can create some unexpected behaviors. Whether those behaviors are useful for solving computing problems is up for debate—the author says that they created the language “as an exploratory game.” Certainly any application built around time might benefit, but only if there’s a need to manipulate historical values at time stamps instead of just recording them.

While Mariposa caught a fair amount of attention recently, it’s not the first implementation of time travel in programming. There is a Haskell package appropriately called tardis, which creates two state transformers: one travels forward in time and one backward. As the docs explain, “The most concise way to explain it is this: getPast retrieves the value from the latest sendFuture, while getFuture retrieves the value from the next sendPast.” One function’s past is another one’s future.

Manipulating values programmatically might allow for some interesting logic, or it might be a novelty. However, traveling through time when debugging code has real benefits and a history stretching back at least to Smalltalk. Current frameworks that include time-traveling debugger implementations include Elm, a functional programming-based frontend system, and Redux, a state container for JavaScript applications, which uses log records to recreate any point in time. There are plenty of implementations of these debuggers for other systems, including WinDbg (Windows), rr (Linux), and Undo (Linux).

Time-traveling programming languages change the values of variables in previous or future states. But if you’re working with a lot of values, you’re probably using a database instead of in-memory variables. In temporal databases, transactions are never overwritten, just timestamped. Plenty of databases include temporal features, including PostrgreSQL, IBM’s Db2, and Snowflake.

While the above languages, debuggers, and databases are trying to manipulate states across time (colloquially, “time travel”), computer science and programming has long sought to model time into a formal logic that can be used in a more deterministic manner than just timestamping with DateTime. Concurrency, specifically the verification of shared-variable concurrency systems, has been a long-standing concern of software engineering. There’s even a yearly conference dedicated to it.

Formal logic developed systems to reason about time, including interval temporal logic (ITL), which was originally developed to specify and verify hardware designs. It uses finite sequences and assumes linear time, so is useful for verifying multithreading logic in hardware. In fact, ITL has been incorporated in the hardware verification language e.

One of the earliest languages using ITL Tempura, currently developed as (Ana)Tempura. Tempura was originally developed originally by Roger Hale, but is now maintained by Antonio Cau and Ben Moszkowski, with the most recent release coming in September 2023. There are applications for voice over IP, runtime monitoring, and artificial intelligence. While it’s grown into a more complete language, the site bills it more of a way to verify “whether a system satisﬁes timing, safety or security properties expressed in ITL. The assertion points are inserted in the source code of the system and will generate a sequence of information (system states), like values of variables and timestamps of value change, while the system is running.”

A number of additional, possibly defunct programming languages used various temporal logic specifications to verify software and hardware logic. Tokio used ITL, while Templog and Chronolog used linear-time logic, and Temporal Prolog is based on linear and branching time temporal logics. All of these grew out of Prolog, a programming language designed for logic programs. According to Dr. Cau, that’s one of the major differences between these languages and Tempura: “The Prolog interpreter has a backtracking mechanism so it can handle nondeterministic specifications. The Tempura interpreter has no backtracking mechanism.”

Working with these languages means overcoming a pretty steep learning curve and understanding the concepts and notation of whatever temporal logic system the languages use. In the forward to the special edition to the Annals of Mathematics and Artificial Intelligence issue on ITL from 2014, the editors remarked, “ITLs are often regarded as being either conceptually or computationally too complex for practical deployment.” As such, there have been a number of modeling, analysis, and verification languages/tools that allow temporal and state modeling without requiring temporal logic understanding:

TLA+: A high-level language for modeling programs and systems, particularly distributed systems, based on mathematics.
Alloy: A software language and analyzer to model programs and check the consistency of software designs. It was inspired by the Z specification language and Tarski’s relational calculus and was influenced by modeling languages like UML.
Promela and SPIN: A modeling language for concurrent systems, which is used with the SPIN model checker to verify properties of these models.
UPPAAL: A tool for modeling, validating, and verifying real-time systems by representing them as networks of timed automata. It’s less a programming language, more a visual simulation tool.
Event-B: A formal method for system-level modeling and analysis that uses set theory and mathematical proofs to verify system consistency.
Maude: A high-level language that uses both equations and rewriting logic, which deals with state changes in concurrent systems.

The majority of these temporal logic languages and modeling systems focus on getting the timing right for state changes within multithreaded, concurrent systems operating fully in the present. In the next section, we’ve going to take a look at some theoretical ideas that treat actual past and present states as resources a program can access in the present.

While time-travel is not currently possible, general relativity theory does suggest time could move in both directions, so physicists have been trying to sort out the math that would make it possible. All sorts of wild stuff has been offered, from super-dense objects of infinite length rotating at one quarter of the speed of light to mirrors that reflect waves backward in time.

With these calculations and speculations, physicists also took arguments about the grandfather paradox from the realm of late-night dorm rooms to academic journals. In a 1979 book (translated to English in 1983), theoretical astrophysicist and cosmologist Igor Novikov speculated that “closed time-like curves” may allow for travel backward in time so long as the data in the curve remained self-consistent, either because it already existed or because the state of the past was adjusted to square up. This is the Novikov self-consistency principle, which Larry Niven fans may know as the law of conservation of history.

Computer scientist and futurist Hans Moravec saw that and imagined a way to exploit it to solve complex problems quickly. With time-loop logic, Moravec suggested that, using a circuit with a negative time delay, you could calculate a result that would be sent back to the initial time and state. In order to not violate the Novikov principle, the correct answer would appear immediately. The catch, as later papers would explore, is that many of these complex problems would be reduced to the halting problem; that is, determining whether the computer would ever be shut down or turned off. If you’re calculating the best results and sending them back in time, you still have to do the calculations in the future. Call it Bill and Ted’s Executing Adventure.

If you want code samples of time-loop logic, someone going by the handle marak has created those. This theoretical program would be available through Node.js, thanks to its aptitude for concurrent processing. It would be a brute-force password cracker, which given a computer that could run forever, could crack nearly any encryption scheme. The possibility of quantum computers has already sent security researchers scrambling for more secure algorithms; could you imagine the havoc of time-loop brute-force cracking?

Fortunately, any actual time travel is still in the realm of the theoretical. You can play with some of the languages we described in this piece to use some interesting programming concepts that break the linear flow of a program or get four-dimensional views of hardware and software state, but you can’t send tomorrow’s lottery numbers back in time.

Yet.

logic articles