Two additional research directions

Independently of the tasks mentioned above, two important research problems are worthy of consideration.

  1. The first problem concerns the extension of our model by the mechanisms of concurrency. Fully denotational models of concurrence are not known today, although there are some attempts to “semi-denotational” models where a denotational semantics is mixed with an operational one.
  2. The second problem has not been probably tackled at all and concerns the construction of semi-formal languages for the description of user-oriented specifications of programs. So far all approaches to program correctness — including ours — are limited to the compatibility of program code with its formal specification. It does not exhaust the reliability problem in the IT industry, because many problems are due to poor communication between a designer of a system and its user. Most probably many area-oriented languages of specifications would be needed.