The Why of Juvix: On the design of smart contract languages

Image source: Aditya via Wikimedia Commons, CC-BY-SA 3.0

In addition to protocol development, in the past several months METASTATE has embarked upon a new project: research & development of a novel smart contract language, Juvix.

Juvix is designed to address the problems that we have experienced while trying to write & deploy decentralised applications and that we observe in the ecosystem at large: the difficulty of effective verification, the ceiling of compositional complexity, the illegibility of execution costs, and the lock-in to particular backends.

In order to do so, Juvix draws upon and aims to productionise a deep reservoir of prior academic research in programming language design & type theory which we believe has a high degree of applicability to these problems.

There should be a substantial bar to meet before electing to write a new language. After investigating many simpler approaches and developing distributed ledgers & smart contracts ourselves, we've decided that this bar, for the use-case of smart contracts on public ledgers, is met — there are many unique, fundamentally difficult problems which can be convincingly solved at the language level, but only by designing & engineering a language and compiler stack from scratch.

This post, the first part of a two-part series, explains the background of considerations and requirements that motivated us to design a new language.

Desiderata

What problems that we observe within the decentralised application ecosystem at large could be addressed at the language level?

Were one to imagine the ideal smart contract language, what features would it have?

Start with a pure functional basis

Many of the observed mistakes & bugs in smart contracts are not specific to the blockchain use-case at all — they are just common errors made in imperative languages by programmers everywhere: unintentional side-effects, type mismatches, and failure to handle exceptions or unexpected states.

Pure functional languages, with strongly-typed terms, immutable data, first-class functions, and referential transparency, are the right basis for a contract language. A strong typesystem enables the typechecker to catch many errors at compile time which would have otherwise resulted in misbehaviour at runtime. Purity, immutable data & referential transparency simplify the mental context a programmer must have, since they no longer need to reason about side effects. First-class functions allow the modularisation of complex logic into individually digestible, composable parts.

Enable an ecosystem of verification

"Formal verification" has been rendered a bit of a buzzword, but the actual need remains mostly unaddressed: a mathematically sound, legible way for users of decentralised applications to reason about what their interactions with an application will or will not do: whether a token really behaves like a currency, whether an exchange contract could accidentally steal their funds, or whether a derivative will always be sufficiently collataralised. A motivating historical example: had it been done, constructive verification of a "spendability" property would have found the Parity multisignature bug.

Exposing formal verification tooling to contract developers is necessary, but not sufficient — it must be possible for third-party software providers, such as wallet authors & application frontend developers, to embed proof-checking into their application and translate success or failure of verifying particular behaviours into legible UI elements — a green checkmark if the token contract is compliant, a red warning otherwise.

Contract property verification must be progressive — proof-construction UX improvements notwithstanding, it will always make little sense to invest time to verify beta applications or experiments. Developers must be able to write contracts, modify them, and progressively verify properties over time, often after the original code has been written.

The state machines of blockchains must eventually understand this verification system, and use that understanding to allow contracts to reason about how other contracts with which they interact will or will not behave, just as users can, and elect only to interact with contracts which can prove that they fulfil certain properties. This will require seamless integration of the verification system into the language itself.

Eliminate the compositional complexity ceiling

Distributed applications are most compelling, and most competitive with their centralised brethren, when they can benefit from the network effects of permissionless interoperation without the bottlenecks of trusted organisational relationships: anyone in the world can deploy a new contract which interacts with yours, perhaps to provide a new feature or application which you hadn't even conceived of. Alas, this potential network effect is severely curtailed by the sheer difficulty of reasoning about complex, multi-layered compositions of contracts.

Because present languages cannot provide checkable guarantees about the behaviour of their own terms, each line of code in a contract must consider what every other line of code might do — to first order, this renders the mental cost of reasoning about the correctness of a contract quadratic in the size of the codebase.

Developers must have the ability to articulate predicates which tightly constrain the behaviour of its own terms in the language itself, and thus eliminate entirely the necessity of tracking the behaviour of some particular dependency, since it has been constrained to exactly what is required and no more.

Provide predictable resource consumption

Resources consumed while executing contracts on replicated ledgers must be paid for. Illegibility and unpredictability of such payments are at present a major UX friction point for contract developers and application users alike. In the past two weeks, about $7500 worth of ETH was wasted due to transactions with insufficient gas allocations. A detailed analysis found that over 90% of Ethereum contracts failed to implement simple optimisations which would have reduced gas costs & saved their users money.

The resource cost of calling a contract must be exactly calculable or at least closely bounded prior to executing the call, so that developers can compare the costs of different code-paths at compile time and users can ensure that they have provided sufficient payment for complete execution. Should the ledger elect to integrate the typechecker into the state machine logic directly, it should be possible to perform these resource cost verifications instead of metering gas at runtime.

Abstract away from particular backends

Blockchains come & go, and the virtual machines or execution environments which they provide improve & change over time. Developers of decentralised applications should be able to abstract over these implementation particulars and write contracts at a sufficiently high-level to capture instead the essential semantics of their intentions, then redeploy these contracts to multiple ledgers and updated execution environments without rewriting them each time.

Optimisations for particular execution environments or ledgers should be logically centralised, handled once by updated compiler pipelines instead of individually by each application developer. Successful abstraction will empower not only contract developers but also protocol engineers: virtual machines can be upgraded more quickly if contracts can easily be recompiled to target new ones, and exit costs of particular ledgers will be reduced if contract code can be re-targeted to other ones.

Retain efficient execution

Execution of contract code is expensive, whether replicated across validation nodes of a distributed ledger, or simulated within the restricted setting of an interactive prover. Formal verification, resource consumption proofs, and backend abstraction must not come at the cost of runtime performance penalties. This is the primary reason for our decision to write a language from scratch — prior work attempting to write an LLL backend for Idris found the resulting code far too inefficient for actual usage. The unique properties of the smart-contract use case — small code sizes and infrequent deployment — should be leveraged to enable optimisations which might not be feasible in a more general-purpose language.

Next up: ingredients & architecture

Juvix aims to satisfy the requirements described in this post by combining novel ingredients from the programming language & type theory literature with pragmatic architectural design choices. The next post in this series will explain in detail these ingredients & design choices and how we think they will enable the language to realise these aims.

Written by Christopher Goes, co-founder of Metastate.

Metastate has ceased its activities on the 31st of January 2021. The team members have joined a new company and working on a new project. If you're interested in programming language theory, functional programming, type theory, formal verification, or compiler engineering positions, check out the open positions at Heliax.

If you have any feedback or questions on this article, please do not hesitate to contact us: hello@heliax.dev.