Juvix synthesizes a high-level frontend syntax, dependent-linearly-typed core language, whole-program optimisation system, and backend-swappable 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 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.
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.
For more design details, see the language reference.
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.
Stack required. 8GB RAM required for stack installation.
- For Ubuntu :
apt install stack - For Debian :
apt install haskell-stack - For Arch Linux :
pacman -S stack - For macOS :
brew install haskell-stack - For Windows, following the instructions here.
After cloning Juvix into a local directory, go into the local Juvix directory, and build and install the binary to the local path with:
makeExpect the installation to take some time. For Windows users: to be able to use the command make, please visit this link.
For full optimisations (but slower compile times):
make build-prodSee the tutorials and documentations on the Juvix website.
Install the Juvix package to get syntax highlighting support for Juvix in VSCode.
Other IDE supports will be added over time.
If you found a bug please open an issue and detail the bug. We will fix it as soon as we can.
We welcome contributions to the development of Juvix. See CONTRIBUTING.md for contribution guidelines.
Ormolu required for source formatting. Run
stack install ormolu to get the latest version (0.0.3.1).
Roswell is required for automatic generation of documentation in doc/Code.
Once Roswell is installed one only needs to add ~/.roswell/bin to their bash path along with running ros install heliaxdev/org-generation.
Then run scripts/precommit.sh.
To open a REPL with the library scoped:
make repl-libTo open a REPL with the executable scoped:
make repl-exeWe would love to hear what you think of Juvix! Join our community:
- Follow us on Twitter
- Subscribe to our newsletter