itchibon777/juvix

A more elegant language for a more civilized age.

Juvix

_{^{(Aditya via Wikimedia Commons, CC-BY-SA 3.0)}}

Overview

Juvix synthesizes a high-level frontend syntax, dependent-linearly-typed core language, and low-level parallelisable optimally-reducing execution model into a single unified stack for writing formally verifiable, efficiently executable smart contracts which can be deployed to a variety of distributed ledgers.

Juvix's compiler architecture is purpose-built from the ground up for the particular requirements and economic trade-offs of the smart contract use case — it prioritises behavioural verifiability, semantic precision, and output code efficiency over compilation speed, syntactical familiarity, and backwards compatibility with existing blockchain virtual machines.

Please note: the frontend language is not yet implemented as we are still working out some details of the type theory & compiler transformations. Juvix may end up supporting an existing frontend language (or more than one).

For details, see the language reference.

Caveats

This is pre-alpha software released for experimentation & research purposes only.

Do not expect API stability. Expect bugs. Expect divergence from canonical protocol implementations.

Formal verification of various properties of the Juvix language & compiler in Agda is in progress but not yet complete.

No warranty is provided or implied.

Juvix is presently executed by a resource-tracing interpreter.

Backends for the EVM, WASM, Michelson, and LLVM are planned but not yet implemented.

Contributing

See CONTRIBUTING.md.

Installation

Requirements

The following are required:

• Stack
• z3
• libff
• libsecp256k1
• Openssl Libssl API
• LLVM9

Instructions for Linux

• Stack
  • For Ubuntu/Debian : apt install stack
  • For Arch Linux : pacman -S stack
• Z3
  • make build-z3 while in the juvix directory
• libsecp256k1
  • For Ubuntu/Debian : apt install libsecp256k1-dev
  • For Arch Linux : pacman -S libsecp256k1
• Openssl Libssl API
  • For Ubuntu/Debian : apt install libssl-dev
  • For Arch Linux : pacman -S openssl
• LLVM9
  • For Arch Linux : pacman -S llvm

Building

Build Juvix and install the binary to the local path with:

make

Building with optimisations

For full optimisations (but slower compile times):

make build-opt

Usage

Juvix is not yet production-ready. You can play around with some functionality in an interactive REPL:

juvix interactive

Development

Ormolu required for source formatting.

Quicklisp and sbcl required for the automatic generation of documentation in doc/Code.

To open a REPL with the library scoped:

make repl-lib

To open a REPL with the executable scoped:

make repl-exe