rchain

RCHAIN

Scalable, Secure, Sustainable
What is LADL?
LADL is a process to create spatial-behavioral type systems. Such a system not only describes the structure of datatypes, but also the behavior of the processes.
LADL and DAO
In 2016, the DAO lost $50M worth of ETH due to someone exploiting a race condition in a wallet contract. In a type system produced by LADL, one can declare that a contract should not contain a race. The compiler can check the code and guarantee that the contract is not susceptible to this kind of attack.
Logic As a Distributive Law
The implementation of a type in a programming language is describing a collection of values for that type. The class Natural, for instance, combines digits using juxtaposition. We can express types as "terms over collections". In many languages, we can, for instance, describe an employee class as follows:

{ "first": String, "last": String, "age": Natural, "salary": Natural }.

Compare this to an instance of the employee class:

{ "first": "Joe", "last": "Schmoe", "age": 35, "salary": 100000 }.

They're exactly the same, except that the class definition has types instead of values. Here's another example where the types are small enumerations:

Suit = [ "Club", "Diamond", "Heart", "Spade" ]
Value = [ "A", "2", "3", "4", "5", "6", "7", "8", "9", "J", "Q", "K" ]
Card = {"suit": Suit, "value": Value }

If we think of the type Card as a collection, how many elements does it have? Well, there are four suits and thirteen values and 4 * 13 = 52, so fifty-two cards in all.
Now suppose we have a data structure that defines a term in a programming language, a syntax tree. We can describe collections of programs in exactly the same way: we simply replace parts of the program with collections that say what's allowed in that position. And just as we multiplied together the ways to make a suit with the ways to make a value in order to get a card, we'll be taking the product of all the collections that appear in the syntax tree. A contract in Rholang can describe the kind of sourcecode it's willing to run!
We can think of adding things to a collection as being analogous to adding numbers, while we can think of the term constructors in the language as being analogous to multiplication. Then just as we have a distributive law that takes products of sums to sums of products,

(a + b)(c + d) = ac + ad + bc + bd

we have a way of turning an expression that involves terms with collections in them (like the class definitions above) into a collection of terms.
This is the core of the LADL algorithm, but there's more. The description of a programming language includes not only its grammar, but also the reduction rules. By allowing class definitions to talk about reduction rules as well as the structure of code, we can describe behaviors. Many security properties can be expressed in terms of behaviors, like "This code does not have a race condition", or "This name is never sent on a channel outside this namespace."
LADL can generate a spatial-behavioral type system for any programming language, but the formulae it generates are practically unusable by anything but formal verification systems unless the language has been designed with LADL in mind, like Rholang has.