[rtpg]

I'm really not a fan of TLA+'s tooling, but I do really love the temporal logic. I've always kinda wanted that stuff in other proving languages, but I don't know how possible it is.

Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling?

(Aside: I have a TLA+ book, but it's notably missing really much in terms of exercises or anything. If anyone has any recommendations for a large set of exercises to play around in the space I'd love to hear about it!)

EDIT: turns out just searching for "temporal logic in X language" gets you papers, found this one paper for axiomatizing temporal logic that seems to be a good starting point for anyone looking at this [0]

[0]: https://lim.univ-reunion.fr/staff/fred/Enseignement/Verif-M2...

[zozbot234]

> Would it be actually possible to write something like an "a la carte temporal logic library" for other proving languages that could get you some of the confidence you can get from TLA+'s modeling?

Temporal logic is just a specific instance of a modal logic, which can be modeled with reasonable ease using a "possible worlds"-based encoding. Note that TLA+ combines temporal logic with non-determinism, which is a different modality.