Temporal logic as a programming language paradigm?

Question

So I'm aware there's some degree of timing-based logic in existing programming languages, like threads and the sleep() function (and derivatives thereof), as well as events / delegates.

However, I was curious about the potential of a language, or at least a library / extension of an existing language, that embraces the concepts of temporal logic as a full-fledged methodology for programming?

For example, a was operator that checks equality for a variable not only in the present moment, but whether it was equal to a value at some previous state in the program too, possibly within a specified period of time before the present moment if the entire history doesn't need to be checked. Or a has been operator that works similarly, but checks to see if the variable has continually held a state for a certain period of time, without changing anywhere in between.

I can already guess the reasons for temporal logic never taking off as a paradigm very likely involve memory, as keeping track of previous program states would likely require a ton of it, to the point of being impractical for anything other than the smallest programs. I would say that could be mitigated by giving the programmer control over which variables get their history tracked (if at all, perhaps through the use of a keyword, like temporal int someValue that explicitly tells the program that its state should be recorded), and even specifying how frequently their state is recorded, which could also improve performance; for example, you could tell a variable to only update every 5 seconds, if you know it doesn't change often and having a high amount of temporal resolution isn't important. Basically, giving the programmmer the power to set certain variables as "recordable", how frequently they should save their history (time resolution), and how far back in the past to check when checking for past values.

That being said, there are probably other reasons why temporal programming doesn't work that I can't think of (but am interested in learning about). Nevertheless, if memory capabilities grow to the point where such temporal paradigms become practical for large-scale projects, could it have potential compared to the existing solutions for managing time in programs? I've read up a tiny bit on it but surprisingly never saw much discussion about it when searching online, other than a paper written on the topic and an old Reddit post where someone actually did make a temporal logic construct for C++, although it's the only one I could find.

Answer 1

TLA+ isn't so much a general purpose language, but...

One of the benefits of using TLA+ to investigate the bug is that once you can reproduce the bug, it’s easy to try alternative fixes. The bug in question is rare and took years to be uncovered, so how would you know if your fix doesn’t introduce another subtle bug that will take years to discover? With TLA+ you can check all possible code paths through your code, giving you a lot more confidence.

It includes such temporal operators as:

• <> ("eventually"),
• ~> ("leads to"), and
• <>[] ("stays")