On Corda's own experimental "arrangement" DSL vs DAML

[gyorgybalazsi]

Simon Maxen compares the way how the “initiate and accept” pattern can be expressed with Corda’s Kotlin smart contracts and DAML, in the excellent blog post How To Have Your Cake and Eat It with DAML-on-Corda.

The Corda people are aware of the fact that their platform could use a proper DSL for smart contracts, or as they say “arrangements”.

The Corda technical white paper in the “12 Future work” section says the following (even mentioning a famous early Haskell based approach for modeling financial contracts):

12.3 Domain specific languages

Domain specific languages for the expression of financial contracts are a popular area of research. A seminal work is ‘Composing contracts’ by Peyton-Jones, Seward and Eber [PJSE200031] in which financial contracts are modelled with a small library of Haskell combinators. These models can then be used for valuation of the underlying deals. Block chain systems use the term ‘contract’ in a slightly different sense to how PJSE do but the underlying concepts can be adapted to our context as well. The platform provides an experimental universal contract that builds on the language extension features of the Kotlin programming language. To avoid linguistic confusion it refers to the combined code/data bundle as an ‘arrangement’ rather than a contract. A European FX call option expressed in this language looks like this:

The programmer may define arbitrary ‘actions’ along with constraints on when the actions may be invoked. The zero token indicates the termination of the deal.

As can be seen, this DSL combines both what is allowed and deal-specific data like when and how much is allowed, therefore blurring the distinction the core model has between code and data. It builds on prior work to enable not only valuation/cash flow calculations, but also direct enforcement of the contract’s logic at the database level as well.

12.3.1 Formally verifiable languages

Corda contracts can be upgraded. However, given the coordination problems inherent in convincing many participants in a large network to accept a new version of a contract, a frequently cited desire is for formally verifiable languages to be used to try and guarantee the correctness of the implementations.

We do not attempt to tackle this problem ourselves. However, because Corda focuses on deterministic execution of any JVM bytecode, formally verifiable languages that target this instruction set are usable for the expression of smart contracts. A good example of this is the Whiley language by Dr David Pearce32, which checks program-integrated proofs at compile time. By building on industry- standard platforms, we gain access to cutting edge research from the computer science community outside of the distributed systems world.

I didn’t try Corda’s own experimental DSL, but as the example shows it’s much less readable than DAML and there is no mention of the “propose and accept” pattern.

Corda doesn’t advertise this experimental DSL actively, and now that we have DAML on Corda, they can treat their homework completed by Digital Asset.

[bernhard]

Fun fact: DAML was heavily inspired by ‘Composing contracts’ by Peyton-Jones, Seward and Eber [PJSE200031], too, and early versions of DAML looked more similar to what you show above than to today’s DAML. Just for fun, here’s a snippet from an early pre-public version of DAML:

iouChf =
  \(owner :: Party) (obligor :: Party) (amount :: Integer) ->
    {@ DESC
       "IOU " <> toText obligor <> " --[" <> toText amount <> "]--> " <> toText owner
    @}
    await
--      [ "description": owner chooses then { "iou": iouChf owner obligor amount }
      { "settle":
        owner chooses account :: Text at tstart then
          { "cash" : settleInChf owner obligor amount account tstart
          }

      , "sell":
        owner chooses newOwner :: Party then
          { "iou": iouChf newOwner obligor amount
          }
      }
  ;

Almost unrecognizable!

[gyorgybalazsi]

I like the current version of DAML much better!

Another fun fact:

Nick Szabo in his paper A Formal Language for Analyzing Contracts (which also can be called seminal) also mentions the “Composing contracts” article but dismisses it as being too narrowly fiance focused:

our language incorporates a wide variety of contractual terms, not just abstract monetary terms and their derivatives. These two characteristics make our language very different from special purpose financial contract languages such as[4]. While we use several financial contract examples to introduce our language and demonstrate its flexibility, its scope both in functionality and the kinds of contracts and transaction protocols it can represent is far broader.

The footnote refers to the mentioned “Composing contracts” article:

4. Composing contracts: an adventure in financial engineering – A different kind of language for specifying financial contracts in order to compute their risk and value.

Szabo, as fas as I know, never implemented his idea of a formal language for smart contracts. He refers to the E programming language as an implementation option, but this seems to be a dead end.

Congratulations to you guys for picking up the initiative and also following through on it! This is what makes the difference between dreamers and achievers.

[sofusmortensen]

The experimental DSL in Corda is something that I contributed in 2016 while I was working as a quant as Nordea. Back in 2015 I was representing Capital Markets of the Bank in R3 Distributed Ledger Group, and was presented a rather complete PoC that evolved to be Corda.

I didn’t like the way contracts were expressed in Corda - wanting something where the contract it self was a first class entity, something I could easily map to the banks own contract scripting language used for risk and pricing. At the time wanting to change Corda, I took the route of helping to accelerate the development to get the stage where the problem I predicted would be become evident to most. This meant implementing the first iteration of being able to dynamically load JVM classes for contracts written in Kotlin. (I became the first from outside R3 to push actual code changes to Corda). Along the way I realised that I could the effect I wanted by writing another smart contract language inside the contract language of Corda. And this is how the DSL came to be.

I never got it finished, as I was hired by Digital Asset in 2017 to work on DAML instead.

Yes - I am biased - but I really find DAML a lot easier for writing smart contracts than Corda. Also I find it elegant that DAML contracts unites both what is done in Corda with Contracts and the Flows for orchestrating the contracts.

Incidentally what the experimental DSL did for representing bespoke OTC’s, you can really do straight in DAML. And I have been doing a couple PoC’s to create improved version in DAML - I hope to soon get the time to dig it out and freshen it up for publication.

[gyorgybalazsi]

Great, @sofusmortensen congratulations for your contributions!

[sofusmortensen]

Here’s what the code as the Corda DSL example could like in a DAML based DSL:

cordaExample = script do

  acmeCorp <- allocateParty "acme corporation"
  highStreetBank <- allocateParty "high street bank"


  let european_fx_option =

        options do
          writerGiven (after maturity) "expire" void        
          given true "exercise" $ options do
            anyGiven (after maturity) "execute" do
              payout "EUR" 1000000
              give $ payout "USD" 1200000

        where
          maturity = lit $ cutLondon $ date 2020 Dec 1


  -- setting up the actual DAML contract (wasn't in the Corda example):
  prop <- submit highStreetBank $ createCmd MultiSign
    with 
      signed = [highStreetBank]; toSign = [acmeCorp]
      contract = createAgreement 
          acmeCorp highStreetBank None (Service highStreetBank "cash") european_fx_option


  submit acmeCorp $ exerciseCmd prop $ MultiSign_Sign acmeCorp

How the contracts reads:
The writer can expire the contract any time after maturity.
The holder can any time (given true) exercise the contract resulting in a new contract that any party can execute given it is after maturity, resulting in a payment from writer to holder of 1000000 EUR, and a payment from holder to writer of 1200000 USD.