Dactylobiotus: The Developer Preview Release of Juvix

Introduction

Smart contract platforms have blossomed in the last few years (see f.i. Ethereum, Tezos, Near, Solana). Due to their novelty and complexity, smart contracts suffer from multiple challenges. Mistakes in smart contracts have led to numerous infamous attacks, resulting in the loss of millions of dollars (see f.i. Yam finance, Balancer’s incident, Bancor’s smart contract vulnerability). Hence, it is crucial to guarantee smart contract safety in order to prevent future disasters. Unfortunately, as pointed out by Philip Daian, ”we simply don’t understand how to build principled, secure smart contract systems yet”[1].

The reason could be that as most smart contract languages have been inspired by mainstream programming languages (in order to smooth the transition for developers to the smart contract world [2]), they are poorly adapted to the blockchain environment. Although significant efforts have been made to reduce security vulnerabilities [3], and numerous possible solutions have been proposed (auditing your smart contract, using meticulous software methodologies, etc.), they don’t address the root problems directly, as evidenced by the numerous hacks that still happen every year (see f.i. bZx oracle exploit on February 14 and February 18, 2020, Dforce hack on April 18, 2020, Akropolis Hack on November 12, 2020) . Thus, a language specifically designed for the blockchain use-case seems to be the best solution to solve this problem. A few proposals already explore this possible solution (see f.i. Vyper or Clarity). Juvix aims to go further down this road by building upon top-notch academic research.

About Juvix and the Dactylobiotus release

Juvix has been designed by Metastate and takes inspiration from Idris, F* and Agda [4], which are dependently typed languages (see this article for a gentle introduction on dependent type programming languages). Juvix’s frontend syntax derives its inspiration principally from ML. The current release, Dactylobiotus, supports compilation to Michelson (virtual machine used for smart contract development on the Tezos platform)[4]. Dactylobiotus supports standard functional syntax, full-spectrum dependent type checking, usage accounting, and compilation all the way to Michelson. A standard library is included containing Michelson's built-in primitive types and operations. Upcoming releases will add support for efficient compilation of Juvix's datatypes and pattern-matching to Michelson and incorporate an algebraic-effects system for writing composable proofs. As the Juvix language is written in a backend-agnostic fashion, future releases will support additional backends.

Fig. 1: Tara the tardigrade (also commonly known as water bear) is Juvix’s mascot. Tara is extremely resilient, and can adapt to various environments.

Juvix features

Juvix is built upon a broad range of ground-breaking academic research in programming language design and type theory [5], among which are dependent types, quantitative type theory and whole-program optimization [6][7].

As with other programs, a smart contract behaves exactly as specified in its code, unfortunately this is not always what the programmer had in mind. Juvix’ goal is to make sure that the code will behave as expected as opposed to other mainstream smart contract languages where the emphasis is on ease of development and deployment. As smart contract mistakes can have dire consequences, it is essential that they are considered like other unforgiving disciplines (e.g. life-support devices, aerospace, etc.). The aim of Juvix is to help write safer smart contracts. To this end it implements the following features as well as other desirable features for a smart contract programming language [5]:

pure functional programming language
formal verification
eliminate compositional complexity ceiling
predictable resources consumption
abstract away from particular backends
maintain efficient execution

For more details about the technicalities please visit the Juvix website or the Juvix Github page (and in particular the language reference). The above features are the reason why Juvix differs from other smart contract programming languages and what led to its creation. At the moment of writing there is no other smart contract programming language that implements all these features. These features make it easier for a developer to ensure that their smart contract behaves exactly as they intend it to.

As Juvix relies on numerous ground-breaking academic research, not that many developers are familiar with those concepts. Thus, at first, it might be more difficult for them to become well-acquainted with Juvix compared to another smart contract language. The Juvix team is well aware of this difficulty and is trying to reduce it (e.g. by using algebraic proof effects (learn more here).

Installation

Juvix can be installed on Linux, MacOS or Windows (for more details about the installation please visit Github). It is currently in a pre-alpha stage of development and only installation from source is supported. As the name of the release indicates, Dactylobiotus is the first developer preview release of Juvix. You should therefore expect bugs. This release is intended for experimentation and research purposes only. No warranty is provided or implied. To help you with this experimentation a syntax highlighting package for Juvix in VSCode has been created (download it here, other IDE supports will follow).

Juvix is an open source project. Contributions are more than welcome (to contribute please follow these guidelines). Please do not hesitate to leave a feedback or report any issues you might encounter.

Conclusion

Due to their novelty and complexity, smart contracts suffer from multiple challenges. Although significant efforts and numerous possible solutions have been proposed to reduce their security vulnerabilities, infamous hacks still happen every year. A language specifically designed for the blockchain use-case seems to be the best solution. Juvix has been created to this end and implements many desirable features for a smart contract programming language. There is currently no other smart contract programming language that implements all these features. These features make it easier for a developer to ensure that their smart contract behaves exactly as they intend it to.

Bibliography

[1] Smart contract security - incentives beyond the launch by phil daian (devcon4) Accessed: 2020-08-13.

[2] Markus Knecht. Mandala: A smart contract programming language. 2019.

[3] Dominik Harz, William Knottenbelt. Towards safer smart contracts: A survey of languages and verification methods. 2018.

[4] Compiling juvix to michelson Accessed: 2020-08-12.

[5] The why of juvix: On the design of smart contract languages Accessed: 2020-08-12.

[6] Juvix language reference Accessed: 2020-08-12.

[7] The why of juvix: Ingredients & architecture Accessed: 2020-08-12.

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.