Rholang is a new programming language that presents many interesting research questions in mathematics, computer science, and software and hardware engineering.
If you would like to work on or fund any research related to rholang, please be in touch.
Hardware to Run the Rho VM
Fully concurrent programming languages such as RChain’s Rholang are based on mobile process calculi like the pi calculus  and the rho calculus . These computation models represent a divergence from traditional computational models such as the lambda calculus or the Turing machine. Yet the ubiquity of the Von Neumann architecture has led to this new generation of computation being implemented as virtual machines which are compiled down to the underlying Von Neumann-based hardware available. This execution technique likely amounts to a performance reduction which may be eliminated by designing new hardware that operates according to the semantics of the concurrent computation model.
Greg Meredith reports that preliminary work on such hardware has been completed using FPGAs.
Compiling Petri Nets to Rholang
Petri nets have long been known to be a valuable resource in expressing workflows. The Statebox project seeks to use petri nets and other similar visual tools to compile down to process-based backend languages. They have expressed interest in using rholang for this purpose.
Currently there is a single mature rholang interpreter, written in scala, and maintained by a small developer team who are simultaneously busy with work on many aspects of the RChain platform. Adding a second implementation will increase the likelihood that the language evolves to meet its potential while giving the existing interpreter a sanity check for correctness. Correctness can and should be guaranteed even more formally.
In order to make mathematically provable claims about code, the semantics must be defined formally. Formal verification is crucial for a smart contract language which can handle high value, irreversible transactions on a blockchain. This work has begun in the K Framework.
Behavioral Type System