Rholang Toward Capabilities Programming

Mike Stay, the CTO of Pyrofex Corp. presented on Rholang. Rholang a strongly typed, concurrent programming lang. for the new blockchain (smart contracts). meetup

Mike Stay on how the type system works with process channels.

Rholang is a new language for writing smart contracts on the Rchain platform. The language is a reflective higher-order process calculus, based on Milner's asynchronous polyadic pi calculus. c2

As such, it is inherently concurrent, which makes it better suited to distributed programming than languages based on Turing machines or Church's lambda calculus, which are inherently sequential.

Rholang will have a spatial-behavioral type system that will enable proving correctness and security properties about the code. While a spatial type describes a class of data structures that are organized in the same way, a behavioral type describes a class of programs that behave in the same way. A behavioral type is a second, coarser way to express programmer intent. The compiler can check whether these two independent expressions of intent are consistent, reducing the number and severity of bugs.

Hard audience questions on deadlocks. Addressed by solving the Dining Philosophers question. Using #Ocap attenuated revocable authority and message passing. Verified using Pi calculus to precompile and spot deadlocks. Using an online compiler. Large OS projects already use multi-servers to build, verify and manage complexity.

Thus why Dr Stay came on board to design the type system. Worked with Mark S Miller at Google (apparently there's a weekly Ocaps meeting that used to be held at HP).

Rholang was written by a graduate student who selected Scala (for it's DSL abilities). Mike is iterating on the type system to knock off the raw edges. Since Scala is based on Java. And Java exploits keep cropping up. Only a minimum of JVM is used to minimize surface area. The goal is get to a Rholang native compiler in couple of years.

To this end Pyrofex is currently a team of 10. 6 PhDs. 4 ex-Googlers, including a compiler engineer. page

Mike received his Ph.D. in Computer Science from the University of Aukland in 2015 with a specialization in category theory. wikipedia

Smart Contracts and Capabilities Up Close by madmode