<p>My answer is really just an elaboration of Gilles', that I had not
read before I wrote mine. Maybe it's nevertheless helpful.</p>

<p>Let me begin my attempt at answering your question with a distinction
between two dimensions of programming languages work that relate quite
differently to programming language theory in general and process
calculus in particular.</p>

<ul>
<li><p>Pure research.</p></li>
<li><p>Product focused research and development.</p></li>
</ul>

<p>The latter typically takes place in industry with the aim of providing
programming languages as a product. The teams developing Java at
Oracle and C# at Microsoft are examples.  In contrast, pure research
is not tied to products. Its aim is to understand programming
languages as objects of intrinsic interest and to explore the
mathematical structures underlying all programming languages.</p>

<p>Because of divergent goals, Different aspects of programming language
theory are relevant in pure research and in product focused R&amp;D The
picture below may give an indication what's important where.</p>

<p><img src="https://i.sstatic.net/KsXqH.png" alt="enter image description here"></p>

<p>One may ask at this point why the two dimensions are so seemingly
different and how they nevertheless relate.</p>

<p>The key insight is that programming language research and development
has multiple dimensions: technical, social and economic.  Almost by
definition, industry is interested in the economic payoff of
programming languages. Microsoft et al don't develop languages out of
the goodness of their hearts but because they believe programming
languages give them an economic advantage.  And they have investigated
deeply why some programming languages succeed, and others, seemingly
similar or with more advanced features, don't.  And they found that
there isn't a single reason. Programming languages and their
environments are complex, and so are the reasons for adopting or
ignoring any specific language.  But the single biggest factor for the
success of a programming language is the preferential attachment of
programmers to languages that are already widely used: the more people
use a language, the more libraries, tools, teaching material are
available, and the more productive a programmer can be using that
language. This is also called the network effect. Another reason is
the the high cost switching languages for individuals and
organisation: mastering language, especially to a not-so-experienced
programmer, and when the semantic distance to familiar languages is
large, is a serious, time-consuming effort.  Given these facts, one
may ask why do new languages get traction at all?  Why do companies
develop new languages at all? Why don't we just stay with Java or
Cobol?  I think there are several key reasons for whey a language does
succeed, and displaces the originally more popular incumbents.</p>

<ul>
<li><p>A new domain of programming opens up that has no incumbents to
displace.  The primary example is the web with its concomitant rise
of Javascript.</p></li>
<li><p>Language stickiness. By this I mean the high price of changing
language. But sometimes programmers move into different fields,
taking a programming language with them, and being successful with
the old language in the new field.</p></li>
<li><p>A language is pushed by a big company with serious financial
firepower. This backing reduces the risk of adoption, because early
adopters can be reasonably sure that the language will still be
supported in a few years. A good example of this is C#.</p></li>
<li><p>A language might come with compelling tools and eco-system. Here too
C# and it's .Net and Visual Studio eco-system could be mentioned as
an example.</p></li>
<li><p>Old languages pick up new features. Java comes to mind, which, in
each iteration, picks up more good ideas from the functional
programming tradition.</p></li>
<li><p>Finally, a new language might have intrinsic technical advantages,
e.g. be more expressive, have nicer syntax, typing systems that
catch more errors, etc.</p></li>
</ul>

<p>Given this background, it should not come as a surprise that there is
somewhat of a disconnect between pure programming language research,
and commercial programming language development. While both aim to
make software construction and evolution more efficient, especially
for large-scale software, industrial programming language work must be
more interested in facilitating quick adoption to reach a critical
mass and get the network effect.  This leads to a research focus on
things that working programmers care about. And that tends to be
things like library availability, compiler speed, quality of compiled
code, portability and so on.  Process calculus as we practise it today
is of little use to programmers working on mainstream projects
(although I believe that will change in the future).</p>

<p>Pure programming language research is quite different. It works with
simplified models of programming languages: the $\lambda$-calculus is
a massive simplification of functional programming. In the same way
the $\pi$-calculus is a massive simplification of concurrent
programming. These massive simplifications are the key to successful
research. They enable us to focus on core computational mechanisms
(e.g. $\beta$-reduction for functional programming,
resolution/unification for logic-programming, name-passing for
concurrent computation). To understand if a language like Scala can
have viable full type-inference, we don't need to worry about the JVM.
Indeed thinking about the JVM will detract from a better understanding
of type-inference. That's why abstraction of computation into tiny
core calculi is vital and powerful.</p>

<p>So you can think of programming language research as a massive sandbox
where people play with toys, and if they find something interesting
when playing with a specific toy, and have investigated the toy
thoroughly, then that interesting toy begins its long march towards
mainstream industrial acceptance. I say long march because language
features first invented by programming language researcher tend to
take decades before becoming widely accepted. For example garbage
collection was conceived in the 1950s and became widely available with
Java in the 1990s. Pattern matching harks back to 1970 and is widely
used only since Scala.</p>

<p>Process calculus is an especially interesting toy.  But it's too new
to be investigated thoroughly. That will take another decade of pure
research.  What currently going in process theory research is to take
the single biggest success story of programming language research, the
theory of (sequential) types and develop the theory of types for
message passing concurrency.  Typing systems of moderate expressivity
for sequential programming, say Hindley-Milner, are now
well-understood, ubiquitous and accepted by working programmers.  We'd
like to have moderately expressive types for concurrent programming.
Research on this started in the 1980s by pioneers like Milner,
Sangiorgi, Turner, Kobayashi, Honda, and others, often based,
explicitly or implicitly, on the idea of linearity which comes from
linear logic.  The last few years have seen a major increase in
activity and I expect this upwards trajectory to continue for the
foreseeable future. I also expect this work to start leaking into
product focused R&amp;D, in parts for the pragmatic reason that young
researchers who have been trained in process calculus will go and work
in industrial R&amp;D labs, but also because of the evolution of CPU and
computer architecture away from sequential forms of computation.</p>

<p>In summary, I would not worry that you don't find cutting edge
programming language theory such as process calculus useful in your
own work of building languages. That's simply because cutting edge
theory does not address the concerns of current programming
languages. It is about future languages. It will take a while for the
'real world' to catch up. The knowledge you use to build languages for
today is the programming language theory of the past.  I encourage you
to learn more about process calculus because it's one of the most
exiting areas of all of theoretical computer science.</p>

CC BY-SA 3.0
2014-07-27T17:05:11.607Z
Wow! How much time did it take to make that diagram, and can I use it in the future?
cody
CC BY-SA 3.0
2014-07-27T17:26:02.230Z
@cody Took a few seconds with OmniGraffle, and feel free to use it.
Martin Berger
CC BY-SA 3.0
2014-06-28T09:26:13.337Z
2014-06-28T09:26:13.337Z
Martin Berger
<p>The science of programming language design is very much in its infancy. Theory (the study of what programs mean and of the expressivity of a language) and empiricism (what programmers manage or don't manage to do) give a lot of qualitative arguments to weigh one way or another when designing a language. But we rarely have any quantitative reason to decide.</p>

<p>There is a delay between the time some theory stabilizes enough for an innovation to be usable in a practical programming language, and the time this innovation begins to appear in “mainstream” languages. For example, automatic memory management with garbage collection can be said to have been mature for industrial use in the mid-1960s, but to have only reached mainstream with Java in 1995. Parametric polymorphism was well-understood in the late 1970s, and made it into Java in the mid-200s. On the scale of a researcher's career, 30 years is a long time.</p>

<p>Wide-scale industrial adoption of a language is a matter for sociologists to study, and that science is even more in its infancy. Market considerations are an important factor — if Sun, Microsoft or Apple pushes a language, this has a lot more impact than any number of POPL and PLDI papers. Even for a programmer who has a choice, library availability is usually far more important than language design. Which is not to say that language design isn't important: having a well-designed language is a relief! It just usually isn't the deciding factor.</p>

<p>Process calculi are still at the stage where the theory hasn't stabilized. We believe that we understand sequential calculations — all the models of things that we like to call sequential calculation are equivalent (that's the Church-Turing thesis). This does not hold for concurrency: different process calculi tend to have subtle differences in expressivity. </p>

<p>Process calculi do have practical implications. A lot of computations out there are distributed — they involve clients talking to servers, servers talking to other servers, etc. Even local computations are very often multithreaded to take advantage of parallelism over multiple processors and to react to environmental concurrency (communication with independent programs and with the user).</p>

<p>Are research advances needed to make better software? After all there's a billion-dollar industry out there that can't tell the pi calculus from a pie in the sky. Then again, that industry spends billions of dollars fixing bugs.</p>

<p>“Will they ever be needed” is never a worthwhile question in research. It is impossible to predict in advance what will have long-term consequences. I would even go further and say that it is a safe assumption that any research will have consequences one day — we just don't know at the time whether that day will come next year or next millennium.</p>

CC BY-SA 3.0
2014-06-15T16:54:55.567Z
2014-06-15T16:54:55.567Z
Gilles 'SO- stop being evil'
<blockquote>
<p>I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications?</p>
<p>The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.</p>
</blockquote>
<p>This is a tricky question! I'll tell you my personal opinion, and I emphasize that this is my <em>opinion</em>.</p>
<p>I do not think pi-calculus is directly suitable as a notation for concurrent programming. However, I think you should <em>definitely</em> study it before designing a concurrent programming language. The reason is that pi-calculus gives a low-level --- but importantly, compositional! --- account of concurrency. As a result, it can express everything you want, but not always conveniently.</p>
<p>Explaining this comment requires thinking a bit about types. First, useful programming languages generally need some kind of type discipline in order to build abstractions. In particular, you need some kind of function type to make use of procedural abstractions when building software.</p>
<p>Now, the natural type discipline of pi-calculus is some variant of classical linear logic. See, for instance, Abramsky's paper <a href="http://www.cs.ox.ac.uk/files/324/pr209.ps.gz" rel="nofollow noreferrer"><em>Process Realizability</em></a>, which shows how you interpret simple concurrent programs as proofs of propositions from linear logic. (The literature contains a lot of work on <em>session types</em> for typing pi-calculus programs, but session types and linear types are very closely related.)</p>
<p>However, I said that the natural type discipline of pi-calculus is <strong>classical</strong> linear logic, and this is the source of the difficulty in using it directly as a programming language. In most presentations of classical linear logic, the (linear) function type <span class="math-container">$A \multimap B$</span> is not a primitive. Instead, you encode function types using de Morgan duality <span class="math-container">$A^\bot ⅋  B$</span>.</p>
<p>This is just fine from the POV type theory, but it's awkward when programming. The reason is that programmers end up managing not just their function calls, but also the call stack. (Indeed, encodings of lambda calculus into pi calculus typically end up looking like CPS transforms.) Now, typing ensures that they will never screw this up, but nevertheless it's a lot of bookkeeping foisted onto the programmer.</p>
<p>This is not a problem unique to concurrency theory --- the mu-calculus gives a good proof-theoretic account of sequential control operators like call/cc, but at the price of making the stack explicit, which makes it an awkward programming language.</p>
<p>So when designing a concurrent programming language, my opinion is that you should design your language with higher-level abstractions than the raw pi-calculus, but you should make sure that it cleanly translated into a sensible typed process calculus. (A nice recent example of this is Tonhino, Caires and Pfenning's <a href="http://www.cs.cmu.edu/%7Efp/papers/esop13a.pdf" rel="nofollow noreferrer"><em>Higher-Order Processes, Functions and Sessions: A Monadic Integration</em></a>.)</p>

CC BY-SA 3.0
2014-06-17T11:04:35.353Z
In what sense to you need to manage the call stack in $\pi$-calculus? This happens automatically in Milner's encoding of $\lambda$ into $\pi$ and also in the new Van Bakel/Vigliotti encoding. Functions are a perfectly fine form of syntactic sugar in $\pi$-calculus.
Martin Berger
CC BY-SA 3.0
2014-06-17T11:07:50.540Z
Also, the $\lambda\mu$-calculus is a really awkward account of sequential control operators like call/cc. Such operators are much more easily and naturally expressed in the $\pi$-caluclus, because jumping is a clearly a form of message passing. $\lambda$-calculus doesn't have a natural notion of name that you can jump to, so you have to code it up as funciton application, or you have to add additional stuff.
Martin Berger
CC BY-SA 3.0
2014-06-17T11:11:08.997Z
One fruitful way of thinking about functions is that they are client-server interactions, where the return channel is affine and the server channel is replicated. This can be typed easily. Session types don't fully capture this, as they are slightly too weak in the constraints on interaction they enforce.
Martin Berger
CC BY-SA 3.0
2014-06-17T11:43:59.380Z
All that said, of course one doesn't want to program in raw $\pi$-calculus any more than in raw $\lambda$-calculus. Both formalism are simplifications that enable us to focus on some features of computation at the exclusoin of others.
Martin Berger
CC BY-SA 3.0
2014-06-17T12:39:21.600Z
@MartinBerger: I was hoping to convince you to answer! I mean that if you wanted to program in raw $\pi$, and also wanted to use functions, then you'd end up writing terms that are in the image of the Milner translation, and so you'd have to "manage the stack" in the sense that you'd essentially be managing continuations and explicit substitutions. (As an aside, I didn't know about the van Bakel/Vigliotti paper -- thanks!)
Neel Krishnaswami
CC BY-SA 3.0
2014-06-17T12:44:21.863Z
IMO a "user-facing" process language should give you lambdas and variables, and (a) show that they have a sensible equational theory in terms of the high-level language itself, and (b) include the desired concurrency primitives, and (c) give an elaboration into a lower-level typed pi-calculus. So this means that a programmer does not have to view functions as sugar, but they are nevertheless conservative over the base calculus, and also the encoding is not interfered with by use of concurrent features (which is the point of designing a concurrent language).
Neel Krishnaswami
CC BY-SA 3.0
2014-06-17T12:54:52.800Z
I'm a bit busy right now, I'll write a bigger answer next week. Explicit substitutions don't need to be managed and managing the continuation is nothing but generating a fresh name,  in other words, a function invocation $let\ x\ = f(17) in ...$ becomes $\overline{f}< 17, (\nu x)r > r(x)....$. It's basically the same thing as in $\lambda$-calculus.
Martin Berger
CC BY-SA 3.0
2014-06-17T12:56:32.730Z
I agree that high-level functions in concurrent languages should have properties (a, b, c). But they do if you use the usual interaction types. See Honda et al's work from about 10 years ago.
Martin Berger
CC BY-SA 3.0
2014-07-25T19:43:04.040Z
@MartinBerger: Which paper of Honda et al?
Uday Reddy
CC BY-SA 3.0
2014-07-27T17:27:11.397Z
@UdayReddy The papers in question are "Strong Normalisation in the Pi-Calculus", "Sequentiality and the Pi-Calculus", "Genericity and the Pi-Calculus" and "Control in the Pi-Calculus".
Martin Berger
CC BY-SA 3.0
2014-06-17T10:32:40.917Z
2014-06-17T10:32:40.917Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>You say that "the <em>true end goal</em> would be to use the theory to actually build a PL."  So, you presumably admit that there are other goals?</p>

<p>From my point of view, the No. 1 purpose of theory is to provide understanding, which can be in reasoning about existing programming languages as well as the programs written in them.  In my spare time, I maintain a large piece of software, an email client, written ages ago in Lisp.  All the PL theory I know such as Hoare logic, Separation Logic, data abstraction, relational parametricity and contextual equivalence etc. does come in handy in daily work.  For instance, if I am extending the software with a new feature, I know that it still has to preserve the original functionality, which means that it should behave the same way under all the old contexts even though it is going to do something new in new contexts.  If I didn't know anything about contextual equivalence, I probably wouldn't even be able to frame the issue in that way.</p>

<p>Coming to your question about pi-calculus, I think pi-calculus is still a bit too new to be finding applications in language design.  The <a href="https://en.wikipedia.org/wiki/Pi-calculus" rel="nofollow">wikipedia page on pi-calculus</a> does mention BPML and occam-pi as language designs using pi-calculus.  But you might also look at the pages of its predecessor CCS, and other process calculi such as CSP, join calculus and others, which have been used in many programming language designs.  You might also look at the "Objects and pi-calculus" section of the <a href="http://books.google.co.uk/books?id=QkBL_7VtiPgC" rel="nofollow">Sangiorgi and Walker book</a> to see how pi-calculus relates to existing programming languages.</p>

CC BY-SA 3.0
2014-07-25T19:34:24.983Z
2014-07-25T19:34:24.983Z
Uday Reddy
<p>I like to search for practical implementations of process calculi in the wild :) (besides reading about the theory).</p>

<ol>
<li>Clojure async channels is based on CSP: <a href="http://clojure.com/blog/2013/06/28/clojure-core-async-channels.html" rel="nofollow noreferrer">http://clojure.com/blog/2013/06/28/clojure-core-async-channels.html</a></li>
<li>Golang also has channels based on CSP (this inspired Rich Hickey for clojure I think): <a href="http://www.informit.com/articles/printerfriendly/1768317" rel="nofollow noreferrer">http://www.informit.com/articles/printerfriendly/1768317</a></li>
<li>There's a guy who made an ACP based extension to scala (Subscript) but I don't have enough reputation to post the link...</li>
</ol>

<p>etc.</p>

CC BY-SA 3.0
2016-11-23T10:13:27.193Z
2016-11-23T10:13:27.193Z
yen wel
<p>For a while now, I have been very interested in programming language theory and process calculi and have started to study them. To be honest, it something that I wouldn't mind going into for a career. I find the theory to be incredibly fascinating. One constant question I keep running into is if either PL Theory or Process Calculi have any importance at all in modern programming language development. I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications? The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.</p>

<pl.programming-languages><process-algebra>
Use of Process Calculi and PL Theory for modern programming language development
Stefan G.
# Use of Process Calculi and PL Theory for modern programming language development

(Asked by: username_0 on 2014-06-14)

For a while now, I have been very interested in programming language theory and process calculi and have started to study them. To be honest, it something that I wouldn't mind going into for a career. I find the theory to be incredibly fascinating. One constant question I keep running into is if either PL Theory or Process Calculi have any importance at all in modern programming language development. I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications? The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.

**Tags:** pl.programming-languages, process-algebra


---

## 5 answers

### Answer by username_1 on 2014-06-28. Score: 10

My answer is really just an elaboration of Gilles', that I had not
read before I wrote mine. Maybe it's nevertheless helpful.

Let me begin my attempt at answering your question with a distinction
between two dimensions of programming languages work that relate quite
differently to programming language theory in general and process
calculus in particular.

* Pure research.
* Product focused research and development.

The latter typically takes place in industry with the aim of providing
programming languages as a product. The teams developing Java at
Oracle and C# at Microsoft are examples. In contrast, pure research
is not tied to products. Its aim is to understand programming
languages as objects of intrinsic interest and to explore the
mathematical structures underlying all programming languages.

Because of divergent goals, Different aspects of programming language
theory are relevant in pure research and in product focused R&D The
picture below may give an indication what's important where.

![enter image description here](https://i.sstatic.net/KsXqH.png)

One may ask at this point why the two dimensions are so seemingly
different and how they nevertheless relate.

The key insight is that programming language research and development
has multiple dimensions: technical, social and economic. Almost by
definition, industry is interested in the economic payoff of
programming languages. Microsoft et al don't develop languages out of
the goodness of their hearts but because they believe programming
languages give them an economic advantage. And they have investigated
deeply why some programming languages succeed, and others, seemingly
similar or with more advanced features, don't. And they found that
there isn't a single reason. Programming languages and their
environments are complex, and so are the reasons for adopting or
ignoring any specific language. But the single biggest factor for the
success of a programming language is the preferential attachment of
programmers to languages that are already widely used: the more people
use a language, the more libraries, tools, teaching material are
available, and the more productive a programmer can be using that
language. This is also called the network effect. Another reason is
the the high cost switching languages for individuals and
organisation: mastering language, especially to a not-so-experienced
programmer, and when the semantic distance to familiar languages is
large, is a serious, time-consuming effort. Given these facts, one
may ask why do new languages get traction at all? Why do companies
develop new languages at all? Why don't we just stay with Java or
Cobol? I think there are several key reasons for whey a language does
succeed, and displaces the originally more popular incumbents.

* A new domain of programming opens up that has no incumbents to
  displace. The primary example is the web with its concomitant rise
  of Javascript.
* Language stickiness. By this I mean the high price of changing
  language. But sometimes programmers move into different fields,
  taking a programming language with them, and being successful with
  the old language in the new field.
* A language is pushed by a big company with serious financial
  firepower. This backing reduces the risk of adoption, because early
  adopters can be reasonably sure that the language will still be
  supported in a few years. A good example of this is C#.
* A language might come with compelling tools and eco-system. Here too
  C# and it's .Net and Visual Studio eco-system could be mentioned as
  an example.
* Old languages pick up new features. Java comes to mind, which, in
  each iteration, picks up more good ideas from the functional
  programming tradition.
* Finally, a new language might have intrinsic technical advantages,
  e.g. be more expressive, have nicer syntax, typing systems that
  catch more errors, etc.

Given this background, it should not come as a surprise that there is
somewhat of a disconnect between pure programming language research,
and commercial programming language development. While both aim to
make software construction and evolution more efficient, especially
for large-scale software, industrial programming language work must be
more interested in facilitating quick adoption to reach a critical
mass and get the network effect. This leads to a research focus on
things that working programmers care about. And that tends to be
things like library availability, compiler speed, quality of compiled
code, portability and so on. Process calculus as we practise it today
is of little use to programmers working on mainstream projects
(although I believe that will change in the future).

Pure programming language research is quite different. It works with
simplified models of programming languages: the $\lambda$-calculus is
a massive simplification of functional programming. In the same way
the $\pi$-calculus is a massive simplification of concurrent
programming. These massive simplifications are the key to successful
research. They enable us to focus on core computational mechanisms
(e.g. $\beta$-reduction for functional programming,
resolution/unification for logic-programming, name-passing for
concurrent computation). To understand if a language like Scala can
have viable full type-inference, we don't need to worry about the JVM.
Indeed thinking about the JVM will detract from a better understanding
of type-inference. That's why abstraction of computation into tiny
core calculi is vital and powerful.

So you can think of programming language research as a massive sandbox
where people play with toys, and if they find something interesting
when playing with a specific toy, and have investigated the toy
thoroughly, then that interesting toy begins its long march towards
mainstream industrial acceptance. I say long march because language
features first invented by programming language researcher tend to
take decades before becoming widely accepted. For example garbage
collection was conceived in the 1950s and became widely available with
Java in the 1990s. Pattern matching harks back to 1970 and is widely
used only since Scala.

Process calculus is an especially interesting toy. But it's too new
to be investigated thoroughly. That will take another decade of pure
research. What currently going in process theory research is to take
the single biggest success story of programming language research, the
theory of (sequential) types and develop the theory of types for
message passing concurrency. Typing systems of moderate expressivity
for sequential programming, say Hindley-Milner, are now
well-understood, ubiquitous and accepted by working programmers. We'd
like to have moderately expressive types for concurrent programming.
Research on this started in the 1980s by pioneers like Milner,
Sangiorgi, Turner, Kobayashi, Honda, and others, often based,
explicitly or implicitly, on the idea of linearity which comes from
linear logic. The last few years have seen a major increase in
activity and I expect this upwards trajectory to continue for the
foreseeable future. I also expect this work to start leaking into
product focused R&D, in parts for the pragmatic reason that young
researchers who have been trained in process calculus will go and work
in industrial R&D labs, but also because of the evolution of CPU and
computer architecture away from sequential forms of computation.

In summary, I would not worry that you don't find cutting edge
programming language theory such as process calculus useful in your
own work of building languages. That's simply because cutting edge
theory does not address the concerns of current programming
languages. It is about future languages. It will take a while for the
'real world' to catch up. The knowledge you use to build languages for
today is the programming language theory of the past. I encourage you
to learn more about process calculus because it's one of the most
exiting areas of all of theoretical computer science.

> **Comments:**
> **username_2**: Wow! How much time did it take to make that diagram, and can I use it in the future?  
> **username_1**: @username_2 Took a few seconds with OmniGraffle, and feel free to use it.  

---

### Answer by username_3 on 2014-06-15. Score: 8

The science of programming language design is very much in its infancy. Theory (the study of what programs mean and of the expressivity of a language) and empiricism (what programmers manage or don't manage to do) give a lot of qualitative arguments to weigh one way or another when designing a language. But we rarely have any quantitative reason to decide.

There is a delay between the time some theory stabilizes enough for an innovation to be usable in a practical programming language, and the time this innovation begins to appear in “mainstream” languages. For example, automatic memory management with garbage collection can be said to have been mature for industrial use in the mid-1960s, but to have only reached mainstream with Java in 1995. Parametric polymorphism was well-understood in the late 1970s, and made it into Java in the mid-200s. On the scale of a researcher's career, 30 years is a long time.

Wide-scale industrial adoption of a language is a matter for sociologists to study, and that science is even more in its infancy. Market considerations are an important factor — if Sun, Microsoft or Apple pushes a language, this has a lot more impact than any number of POPL and PLDI papers. Even for a programmer who has a choice, library availability is usually far more important than language design. Which is not to say that language design isn't important: having a well-designed language is a relief! It just usually isn't the deciding factor.

Process calculi are still at the stage where the theory hasn't stabilized. We believe that we understand sequential calculations — all the models of things that we like to call sequential calculation are equivalent (that's the Church-Turing thesis). This does not hold for concurrency: different process calculi tend to have subtle differences in expressivity.

Process calculi do have practical implications. A lot of computations out there are distributed — they involve clients talking to servers, servers talking to other servers, etc. Even local computations are very often multithreaded to take advantage of parallelism over multiple processors and to react to environmental concurrency (communication with independent programs and with the user).

Are research advances needed to make better software? After all there's a billion-dollar industry out there that can't tell the pi calculus from a pie in the sky. Then again, that industry spends billions of dollars fixing bugs.

“Will they ever be needed” is never a worthwhile question in research. It is impossible to predict in advance what will have long-term consequences. I would even go further and say that it is a safe assumption that any research will have consequences one day — we just don't know at the time whether that day will come next year or next millennium.


---

### Answer by username_4 on 2014-06-17. Score: 3

> I see so many variants on the Pi-calculus out there and there is a lot of active research, but will they ever be needed or have important applications?
>
> The reason why I ask is because I love developing programming languages and the true end goal would be to use the theory to actually build a PL. For the stuff I have written, there really has not been any correlation to theory at all.

This is a tricky question! I'll tell you my personal opinion, and I emphasize that this is my *opinion*.

I do not think pi-calculus is directly suitable as a notation for concurrent programming. However, I think you should *definitely* study it before designing a concurrent programming language. The reason is that pi-calculus gives a low-level --- but importantly, compositional! --- account of concurrency. As a result, it can express everything you want, but not always conveniently.

Explaining this comment requires thinking a bit about types. First, useful programming languages generally need some kind of type discipline in order to build abstractions. In particular, you need some kind of function type to make use of procedural abstractions when building software.

Now, the natural type discipline of pi-calculus is some variant of classical linear logic. See, for instance, Abramsky's paper [*Process Realizability*](http://www.cs.ox.ac.uk/files/324/pr209.ps.gz), which shows how you interpret simple concurrent programs as proofs of propositions from linear logic. (The literature contains a lot of work on *session types* for typing pi-calculus programs, but session types and linear types are very closely related.)

However, I said that the natural type discipline of pi-calculus is **classical** linear logic, and this is the source of the difficulty in using it directly as a programming language. In most presentations of classical linear logic, the (linear) function type $A \multimap B$ is not a primitive. Instead, you encode function types using de Morgan duality $A^\bot ⅋ B$.

This is just fine from the POV type theory, but it's awkward when programming. The reason is that programmers end up managing not just their function calls, but also the call stack. (Indeed, encodings of lambda calculus into pi calculus typically end up looking like CPS transforms.) Now, typing ensures that they will never screw this up, but nevertheless it's a lot of bookkeeping foisted onto the programmer.

This is not a problem unique to concurrency theory --- the mu-calculus gives a good proof-theoretic account of sequential control operators like call/cc, but at the price of making the stack explicit, which makes it an awkward programming language.

So when designing a concurrent programming language, my opinion is that you should design your language with higher-level abstractions than the raw pi-calculus, but you should make sure that it cleanly translated into a sensible typed process calculus. (A nice recent example of this is Tonhino, Caires and Pfenning's [*Higher-Order Processes, Functions and Sessions: A Monadic Integration*](http://www.cs.cmu.edu/%7Efp/papers/esop13a.pdf).)

> **Comments:**
> **username_1**: In what sense to you need to manage the call stack in $\pi$-calculus? This happens automatically in Milner's encoding of $\lambda$ into $\pi$ and also in the new Van Bakel/Vigliotti encoding. Functions are a perfectly fine form of syntactic sugar in $\pi$-calculus.  
> **username_1**: Also, the $\lambda\mu$-calculus is a really awkward account of sequential control operators like call/cc. Such operators are much more easily and naturally expressed in the $\pi$-caluclus, because jumping is a clearly a form of message passing. $\lambda$-calculus doesn't have a natural notion of name that you can jump to, so you have to code it up as funciton application, or you have to add additional stuff.  
> **username_1**: One fruitful way of thinking about functions is that they are client-server interactions, where the return channel is affine and the server channel is replicated. This can be typed easily. Session types don't fully capture this, as they are slightly too weak in the constraints on interaction they enforce.  
> **username_1**: All that said, of course one doesn't want to program in raw $\pi$-calculus any more than in raw $\lambda$-calculus. Both formalism are simplifications that enable us to focus on some features of computation at the exclusoin of others.  
> **username_4**: @MartinBerger: I was hoping to convince you to answer! I mean that if you wanted to program in raw $\pi$, and also wanted to use functions, then you'd end up writing terms that are in the image of the Milner translation, and so you'd have to "manage the stack" in the sense that you'd essentially be managing continuations and explicit substitutions. (As an aside, I didn't know about the van Bakel/Vigliotti paper -- thanks!)  
> **username_4**: IMO a "user-facing" process language should give you lambdas and variables, and (a) show that they have a sensible equational theory in terms of the high-level language itself, and (b) include the desired concurrency primitives, and (c) give an elaboration into a lower-level typed pi-calculus. So this means that a programmer does not have to view functions as sugar, but they are nevertheless conservative over the base calculus, and also the encoding is not interfered with by use of concurrent features (which is the point of designing a concurrent language).  
> **username_1**: I'm a bit busy right now, I'll write a bigger answer next week. Explicit substitutions don't need to be managed and managing the continuation is nothing but generating a fresh name,  in other words, a function invocation $let\ x\ = f(17) in ...$ becomes $\overline{f}< 17, (\nu x)r > r(x)....$. It's basically the same thing as in $\lambda$-calculus.  
> **username_1**: I agree that high-level functions in concurrent languages should have properties (a, b, c). But they do if you use the usual interaction types. See Honda et al's work from about 10 years ago.  
> **username_5**: @MartinBerger: Which paper of Honda et al?  
> **username_1**: @UdayReddy The papers in question are "Strong Normalisation in the Pi-Calculus", "Sequentiality and the Pi-Calculus", "Genericity and the Pi-Calculus" and "Control in the Pi-Calculus".  

---

### Answer by username_5 on 2014-07-25. Score: 2

You say that "the *true end goal* would be to use the theory to actually build a PL." So, you presumably admit that there are other goals?

From my point of view, the No. 1 purpose of theory is to provide understanding, which can be in reasoning about existing programming languages as well as the programs written in them. In my spare time, I maintain a large piece of software, an email client, written ages ago in Lisp. All the PL theory I know such as Hoare logic, Separation Logic, data abstraction, relational parametricity and contextual equivalence etc. does come in handy in daily work. For instance, if I am extending the software with a new feature, I know that it still has to preserve the original functionality, which means that it should behave the same way under all the old contexts even though it is going to do something new in new contexts. If I didn't know anything about contextual equivalence, I probably wouldn't even be able to frame the issue in that way.

Coming to your question about pi-calculus, I think pi-calculus is still a bit too new to be finding applications in language design. The [wikipedia page on pi-calculus](https://en.wikipedia.org/wiki/Pi-calculus) does mention BPML and occam-pi as language designs using pi-calculus. But you might also look at the pages of its predecessor CCS, and other process calculi such as CSP, join calculus and others, which have been used in many programming language designs. You might also look at the "Objects and pi-calculus" section of the [Sangiorgi and Walker book](http://books.google.co.uk/books?id=QkBL_7VtiPgC) to see how pi-calculus relates to existing programming languages.


---

### Answer by username_6 on 2016-11-23. Score: 1

I like to search for practical implementations of process calculi in the wild :) (besides reading about the theory).

1. Clojure async channels is based on CSP: <http://clojure.com/blog/2013/06/28/clojure-core-async-channels.html>
2. Golang also has channels based on CSP (this inspired Rich Hickey for clojure I think): <http://www.informit.com/articles/printerfriendly/1768317>
3. There's a guy who made an ACP based extension to scala (Subscript) but I don't have enough reputation to post the link...

etc.


---

