[lou1306]

Uhm, are they that different, though?

For instance, you can formally express at least a part of the "there should be a button that pulls in new data when clicked" specification. In LTL, that would be something like something like:

[] (buttonClicked -> <>newDataPulled)

(Notice that I switched from actions (click, pull) to states (clicked, pulled), as LTL is a state-based logic.)

[pydry]

Yes.

E.g. according to the article "Specs are math" <-- not in my experience