One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained in some ways, but not as extreme as requiring complete referential-transparency).
It's good to learn about applying types to process calculi. I wasn't aware of that work at all.
Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP
The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.
applying types to process calculi. I wasn't aware of that work at all.
Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.
Moreover, Cury-Howard based approaches really work only for a restricted form of programming: pure and total functions.
Much recent research in programming languages is about types for interacting processes. The most well-known, but by no means only example are the session types pioneered by K. Honda. The key idea is that each process has a bunch of interaction points, and the interaction at each interaction point is constrained by a type. Such types typically
- What direction does data flow? E.g. channel x is used for input while channel y does only output.
- What kind of data is exchanged on the channel? E.g. x is used to exchange a boolean, while y exchanges pairs, the first component of which is a double, and the second component is a channel name which is used for inputing a string.
- How often is a channel used? E.g. x is linear (used exactly once), y is affine (used at most once) while z can be used an arbitrary number of times.
This setup has been investigated from many angles, and one of the most beautiful results in this space is that normal types known from lambda-calculus (e.g. function space) can be recovered precisely as special cases of such interaction types, using Milner's well-known encoding of functional computation as interaction.