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.