Well I do not have time today. So perhaps I can write a little about time. This would be just a memo for me: if unreadable my apologies.
Of course we need to put time into our language --- at some point. How can we set time?
(1) independent timer (this guy throws something when time has come).
(2) we put put explicitly how long it can wait without relying on timer.
(3) we can put this as an assertion
Pros and Cons:
(1) timer:
pros:
This is very flexible and expressive
A lot of people know how to use it
cons:
Very operaitonal
Does not have full expressive power without "atomicity" block in the language
(2) elaboration (annotation) on input etc.
pros:
This is the standard case
Moderately declarative and can do something timer alone cannot do
cons:
Still operational
Is not as flexible as timer --- we may need many kinds of elaborations
(3) assertions or design by contract
profs:
Looks promising
cons:
Perhaps we do not know how to do this generally and cleanly.
* * *
So here is a question: can we use (1) and perhaps atomicity to think about (2) and (3)? That is can we consider what kinds of assertions (design by contract) are there by going back to their operational content?
In either way we need to start from a concrete example (or two). And I do have a concrete example --- on that I will discuss in later posts. Today I do not have much time...to talk about this rather basic subject fully.
