TLA+

I’ll soon be attending Markus Kuppe’s workshop on TLA+ and one of the pre-read materials is Dijkstra’s EWD998 - Shmuel Safra’s version of termination detection. I haven’t read a serious, academic paper since college like 3 years ago1, so it was quite an adventure getting back into the swing of things. As I was reading, I spent a lot of time going back and forth to make things make sense, because the hallmark of a real paper is that you can’t just consume it in one go if you actually want to understand the material....