heliaxdev / Juvix
Programming Languages
Juvix
Overview
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.
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.
Installation
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.
Building
After cloning Juvix into a local directory, go into the local Juvix directory, and build and install the binary to the local path with:
make
Expect the installation to take some time.
For Windows users: to be able to use the command make, please visit this link.
Building with optimisations
For full optimisations (but slower compile times):
make build-prod
Usage
.ju
contract
Writing and compiling your first See the tutorials and documentations on the Juvix website.
Visual Studio Code support
Install the Juvix package to get syntax highlighting support for Juvix in VSCode.
Other IDE supports will be added over time.
Report a bug
If you found a bug please open an issue and detail the bug. We will fix it as soon as we can.
Contributing
We welcome contributions to the development of Juvix. See CONTRIBUTING.md for contribution guidelines.
Installation requirements
Formatter
Ormolu required for source formatting. Run
stack install ormolu
to get the latest version (0.0.3.1).
Documentation Generator
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
.
REPL
To open a REPL with the library scoped:
make repl-lib
To open a REPL with the executable scoped:
make repl-exe
Be part of the community
We would love to hear what you think of Juvix! Join our community:
- Follow us on Twitter
- Subscribe to our newsletter