> I've recently been going through temporal logics. If only more programmers were aware of the beauty of the proof of weak fairness. And its implications in system specifications.

I'm a mathematician and have read about temporal logic. What beautiful proof of weak fairness do you mean here?