> It is natural to ask whether there are applications to program verification. I don’t know, but Dan Ghica and I speculate that there are, and we are planning to investigate this.

I wonder if they got any interesting results from this investigation. There are some practical applications which works on infinite data (such as streams), but I don’t see immediately how this applies there.