8

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.

6
  • 5
    What class of problems that developers run into can you more simply solve by using temporal logic vs the other available approaches. Is that difference enough to justify learning how to solve problems this way, and to extend/implement languages/libraries to support it? Because the temporal logic implementation pointed out is essentially 5 timestamps and a loop checking that they all occurred within x seconds. I would argue it to be equivalent in logically complexity.
    – Kain0_0
    Nov 9 '20 at 0:01
  • 2
    I would distinguish between operations on data with some temporal aspect (like audit trails), and the scheduling of execution. They are fundamentally different problems.
    – Steve
    Nov 9 '20 at 8:31
  • 2
    On this site, most experts prefer to find solutions to problems, not the other way round.
    – Doc Brown
    Nov 9 '20 at 11:55
  • 1
    Correctly synchronized threads don't use timing-based logic (for the management of concurrency, anyway). The temporal logic of mutual exclusion, or atomicity, must be invariant under timing conditions to work, and yet you're introducing real-time concepts and the race conditions that come with them. Why?
    – Useless
    Nov 9 '20 at 12:41
  • 2
    "What class of problems [..] can you more simply solve by using temporal logic?" Here's an example of using TLA+ to understand a concurrency bug in glibc. Nov 10 '20 at 7:53
7

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")

Not the answer you're looking for? Browse other questions tagged or ask your own question.