The development of programming languages with strong foundations in concurrency theory should greatly aid the design, coding, and verification of concurrent systems. Moreover, such an approach could eliminate the gap between the model and implementation of a system, since they would be one in the same.
Designing programming languages for concurrency is nontrivial task. Adding a notion of concurrency to an existing language often breaks some of the tacit assumptions that a language is making about the underlying system, e.g., determinism and no interference on variables. Thus, designing a language with an explicit concurrency model from scratch may be less error-prone.
Having an explicit concurrency model in a programming language also makes the programmer aware of the task at hand and helps making the pitfalls of concurrency, e.g. the introduction of deadlocks or livelocks, more evident to the programmer. If the language is sufficiently expressive it could lead to the construction of re-usable abstractions for sophisticated synchronization mechanisms in much the same way as objects are used in sequential systems today.
Furthermore, a well-designed language could promote portability across a wide spectrum of (network) architectures without limiting parallelism. Languages such as ESTERELLE and Occam have, in their respective domains, proved the viability of this approach.
It is important that the development of models, formalisms, logics, tools and programming languages goes hand in hand, or at least are kept relatively synchronized to avoid divergence and thus defeating the overall objective of being able to verify running code. Currently there is a growing list of initiatives in this direction, to mention a few: Oz, PICT, CML and Facile. This direction of work bears similarities with the efforts of extending concurrency formalisms to capture more non-concurrency aspects, e.g. the current enrichments to LOTOS for describing abstract data types. Joint developments should strongly be encouraged. It is important that the theoretical footing of these languages is seen as an advantage, not as a hindrance. Then concurrency theory will be able to contribute to the creation of better and more reliable mainstream computing systems.
The development of new type systems may also prove fruitful in the quest for programming languages for concurrency. For example, in concurrent object oriented programming, types are augmented with behavioral information. Similarly, we could devise new type systems that guarantee safety and liveness properties in the same way that traditional type systems guarantee safety in calling functions and procedures.
The design of safe and secure languages with a well understood concurrency model is becoming increasingly important now that mobile agents or applets have started to roam the internet. Currently, mobile agents are written in languages such as Java, Telescript or Tcl/Tk, all having rudimentary notions of concurrency based, e.g., on threads and semaphores. There is, however, a growing need for extending the concurrency constructs of these languages or designing new languages with more advanced synchronization mechanisms, based e.g. on synchronous channels, multi-cast groups and constraint variables. Concurrency theory, in particular higher order and mobile theories, can play an important role in helping system designers analyze sophisticated systems based on the mobile agents principle. Although the future for concurrency theory in this direction looks bright, there is still a need for further developments in verification techniques for mobile agents.