A new language for a new paradigm: smart contracts

DAML — a language purpose-built for the exchange of value

In Distributed Ledgers need more than traditional design patterns, Shaul asserted that because Distributed Ledger Technology (DLT) is a fundamentally new paradigm for operating applications that span multiple untrusted actors, programming languages used to build applications for more traditional environments are insufficient for writing smart contracts.

What, then, should a DLT contract language look like?

Successful programming languages become successful for a variety of reasons, but rarely due to the inclusion of a single killer feature. Most programs can be written in most languages, so if a given language lacks a desired feature then the deficiency can usually be worked around. Nevertheless, new people will always want to do new things in new ways. Although it may be possible to use language X to implement system Y, if the programming structures a language provides are not well suited for the task, then the programmer will feel that the ideas they need to express are constrained by the language being used. In this case the programmer will look for a new language, one that provides a better environment in which to express their ideas.

In the words of Ludwig Wittgenstein,

“The limits of my language are the limits of my mind. All I know is what I have words for.”

Financial contracts are not websites, they are not video games, and they are not quadcopter flight control systems. Programming languages that are a good fit for those applications are not necessarily a good fit for financial contracts, because the ideas that need to be expressed, and the properties required of the programs are so different.

Smart contracts are machine encoded promises to perform certain actions. The fulfilment of these promises is then carried out automatically by the distributed ledger system that hosts the contracts, freeing humans from the drudgery of performing actions that they have already agreed to perform. Standard languages are well suited to express standard concepts about data and computation, but the concepts of promise, right and obligation are unique to the domain of contracts.

In their post What properties must an enterprise smart contract language have?, Simon and Neil, our colleagues from the Digital Asset Language Engineering team, laid out five key properties of smart contract systems, which a contract language must enable. Paraphrased, these properties are:

• Proof of rights and obligations
  For the consequences of a contract to be compulsory, entrance must be voluntary, and
  for the processing of a contract to be automated, one must be able to reliably reason about all possible future outcomes of any given state of the contract.
• Confidential execution
  For a contract to be confidential, only the parties affected by the contract can have the right to view contract details.
• Evidentiary trail
  For a contract to be enforceable, incontrovertible evidence of its authorization by all stakeholders must be preserved.
• Formally verifiable
  For a contract to be guaranteed to perform as intended, it must be amenable to formal verification methods.

What properties does your current system have? How do you know?

One imagines that their computing systems have all sorts of properties. “If I add files to this folder then I can access them from home, most of the time.” Or, “If I join a conference call via this website then I can talk to my children, most of the time”. Good software systems allow their users to form a simple mental model of how the system works — but software does not always work, everybody knows. Great software systems also allow their users to form a mental model of the limits of the system, and under what conditions it cannot work.

The ability of both software programmers and software users to form a clean mental model of how a system works depends largely on how clean the abstractions are. For example, when most people use an automobile to transport them somewhere, they prefer not to worry about details like ignition timing and fuel/air mixture. The accelerator pedal is a good abstraction, translating the wishes of the operator into actions by the motor and drivetrain. In a similar way, most smart contract programmers prefer to focus on business logic, rather than low level details such as hashing, cryptography and consensus protocols.

DAML, the Digital Asset Modelling Language, is this smart contract language. DAML has been built specifically for distributed ledgers, and enables the safe, unambiguous and high level specification of real-time business logic.

DAML is a language of contracts, where agreements and the parties to them are native constructs in the language. Using DAML, programmers describe how contracts are formed, which parties have authorized this formation, and which parties have been delegated rights under a contract. DAML expresses contracts, parties, rights, obligations, and authorization directly, which means programmers are free to focus on getting their business logic right, rather than how to encode these ideas as lower level machine constructs. The fact that DAML expresses contracts directly also means that the DAML system itself can reason about the business logic, automatically checking the code for problems involving rights, obligations, and lack of authority.

DAML is a language of privacy, where only the data that a party is authorized to access is revealed to them. As parties and contracts are native constructs in the language, the right of a given party to view the details of a particular contract is a fundamental notion that can be reasoned about directly. The DAML system automatically tracks which parties are authorized to see the details of each contract. This information is then passed through to the underlying distributed ledger system, which ensures that only the data a particular party is authorized to see is sent to their physical node on the network.

DAML is a language of ledgers, where contract data is stored using a structured ledger data model, rather than a foamy sea of binary words. Storing ledger data in its native form frees programmers from the burden of hand encoding their data into an ill-fitting backend storage system. The very execution of a DAML program also creates a structured, human understandable audit trail that explains exactly why each action was performed, and why each party that exercised a choice on a contract had the right to do so.

DAML is a functional language, functions being the building blocks of mathematics, in finance and otherwise. DAML allows programmers to encapsulate business reasoning in strongly typed mathematical functions. DAML supports all the standard functional design patterns, integrated with a clean and well specified ledger model. Strong typing means that the behavior of a function can be automatically checked by the DAML system, helping the programmer reason about how each part of their program will affect the state of the ledger. Strongly typed functional programming is also amenable to formal verification using existing, proven techniques such as those used to verify the correctness of the CompCERT compiler and the seL4 microKernel.

With those design goals and features of DAML in mind, the coming blog posts will be a series of deeper dives into DAML, beginning with a look at how DAML helps ensure that all contracts on a distributed ledger are entered into voluntarily.

Read Part 4: The only valid smart contract is a voluntary one — easier said than done

New to this series about DAML? Click here to read from the beginning!

Join the community and download the DAML SDK at www.daml.com

About the authors

Ben Lippmeier, Ph.D, Senior Software Engineer — Product Foundations, Digital Asset. http://benl.ouroborus.net

Ben Lippmeier works in the team that developed DAML — he wrote the core of the DAML type checker as well as core parts of the DAML runtime system. He holds a PhD in Programming Language Theory from the Australian National University (ANU), has been a researcher at UNSW Australia, and lectured in programming language theory and other areas of computer science at the Australian National University, UNSW Australia, and the University of Sydney. While working on DAML, Ben continues his involvement with academic programming language research, being the program chair for the Haskell Symposium in 2015, and on the program committee for the International Conference on Functional Programming in 2017. Previous projects include work on Data Parallel Haskell, the Discus programming language, and the Iron Lambda suite of formal proofs for functional programming languages.

Edward Kmett, Senior Software Engineer — Language Engineering, Digital Asset. http://comonad.com

Edward works on the design and implementation of DAML with a particular emphasis on the user experience. He holds a collection of degrees from Eastern Michigan University, including Masters’ degrees in Mathematics and Computer Science and graduate certificates in Artificial Intelligence and Bioinformatics. He is particularly active in the Haskell programming language community, where he chairs the Haskell Core Libraries Committee and previously served as the founding vice-president of haskell.org. He chaired the program committee for Commercial Users of Functional Programming from 2014 to 2015 and administered the Google Summer of Code for Haskell for several years. He spends much of his time dragging obscure mathematics not just into practice, but popular use, and is a common keynote speaker at programming conferences worldwide. Previous projects include extensive work on the Scalaz functional programming library for Scala, popularizing the notion of “lenses” across a wide variety of functional programming languages, building the Ermine programming language for S&P Global Market Intelligence, and writing and maintaining over 125 other Haskell libraries for everything from proper hyphenation, to new paradigms for concurrency, to robust numerical methods.