From Rholang Wiki
Jump to navigation Jump to search

Rholang is a new programming language that presents many interesting research questions in mathematics, computer science, and software and hardware engineering.

Get Involved[edit]

If you would like to work on or fund any research related to rholang, please be in touch.

Research Areas[edit]

Hardware to Run the Rho VM[edit]

Fully concurrent programming languages such as RChain’s Rholang are based on mobile process calculi like the pi calculus [1] and the rho calculus [2]. 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. Brief discussion at 37:30 mark

Compiling Petri Nets to Rholang[edit]

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.

Redundant Interpreters[edit]

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.

Formal Semantics[edit]

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[edit]

Traditionally there has been a distinction between statically-typed languages like C, Java, and Haskell and dynamically typed languages like Javascript and Python. The benefits of static typing are clear in the helpful type-checking messages that arise when programming a language like Haskell. However, even these static type systems can reason only about the structure of the data that is passed into or out of a function. By way of example, functions like shuffle, sort, and identity all satisfy the type signature Ord a => [a] -> [a]. A behavioral type system allows the same kind of type-checking on the behavior of a function. So the previous functions could be distinguished by their behavior. This allows the type checker to assist the programmer with compile-time errors to the effect of, “You can’t call the shuffle function because you expected a function that sorts the list, and shuffle doesn’t do that.”