1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-11 08:25:46 +03:00
Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
Go to file
2022-09-26 16:03:36 +02:00
.github Add --allow-different-user to workflow stack command (#1492) 2022-08-30 15:35:45 +01:00
app Autocomplete ".jvc" input files for core {eval, read} commands (#1542) 2022-09-15 16:02:20 +01:00
assets Small changes for the presentation (#1456) 2022-08-17 18:27:42 +02:00
c-runtime Allow _ in Wasm exported names to support Anoma signature (#1449) 2022-08-12 09:06:14 +01:00
docker Add a github action to build a static linux binary (#1488) 2022-08-30 12:18:34 +01:00
docs/org Refactor CLI (#1527) 2022-09-14 16:16:15 +02:00
examples/milestone Make comma a delimiter (#1525) 2022-09-12 11:39:11 +02:00
juvix-mode Refactor CLI (#1527) 2022-09-14 16:16:15 +02:00
juvix-stdlib@5228caaf13 Remove Int from stdlib and update SimpleFungibleToken example (#1414) 2022-07-27 10:24:25 +02:00
licenses Add Haddock and Agda licenses (#1506) 2022-09-06 09:30:01 +01:00
src/Juvix Properly handle top lambdas in the termination checker (#1544) 2022-09-26 16:03:36 +02:00
test Add lambda expressions to internal and add typechecking support (#1538) 2022-09-23 15:43:18 +02:00
tests Properly handle top lambdas in the termination checker (#1544) 2022-09-26 16:03:36 +02:00
.github_changelog_generator Update Changelog v0.2.3 🎉 2022-08-15 12:24:42 +02:00
.gitignore Add Haddock and Agda licenses (#1506) 2022-09-06 09:30:01 +01:00
.gitmodules Rename MiniJuvix to Juvix (#259) 2022-07-08 13:59:45 +02:00
.hlint.yaml Monomorphization (#70) 2022-05-04 10:50:03 +02:00
.pre-commit-config.yaml Fix Changelog links and minors (#1371) 2022-07-14 11:41:58 +02:00
.pre-commit-hooks.yaml Add initial documentation (#119) (#120) 2022-05-23 16:20:02 +02:00
book.toml Rename MiniJuvix to Juvix (#259) 2022-07-08 13:59:45 +02:00
changelog.org Update Changelog v0.2.5 🎉 2022-09-14 18:08:46 +02:00
hie.yaml Rename MiniJuvix to Juvix (#259) 2022-07-08 13:59:45 +02:00
LICENSE First commit, initial project template. 2021-09-26 18:59:51 +02:00
Makefile Fix docs webapp examples CI build (#1505) 2022-09-05 13:38:04 +01:00
package.yaml Bump version to 0.2.5 2022-09-14 17:41:02 +02:00
README.org Add CLI usage examples doc and integrate with README (#1504) 2022-09-01 10:54:38 +01:00
stack.yaml Upgrade to ghc-9.2.4 (#1451) 2022-08-15 16:58:26 +02:00

Juvix

<a href="https://github.com/anoma/juvix/actions/workflows/ci.yml"> <img alt="CI status" src="https://github.com/anoma/juvix/actions/workflows/ci.yml/badge.svg" /> </a>

<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg" alt="pages-build-deployment" /></a>

<a href="https://github.com/anoma/juvix/blob/main/LICENSE"> <img alt="LICENSE" src="https://img.shields.io/badge/license-GPL--3.0--only-blue.svg" /> </a>

<a href="https://github.com/anoma/juvix"> <img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/seating-mascot.051c86a.svg" /> </a>

Description

Juvix is a research programming language created by Heliax as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling validity predicates to the C language, which can be deployed to various distributed ledgers including Anoma.

The Juvix language and related tools are documented in the Juvix book. To write and test Juvix programs, you can use your favorite text editor and the juvix command line tool. However, we recommend using the juvix-mode in Emacs or the plugin in VSCode.

First examples of programs written in Juvix

The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running juvix html --recursive FileName.juvix.

The Juvix standard library contains common functions that can be used in Juvix programs.

Installation

MacOS

The easiest way to install Juvix on MacOS is by using Homebrew.

To install the homebrew-juvix tap, run:

brew tap anoma/juvix

To install Juvix, run:

brew install juvix

Helpful information on the shell can also be obtained by running:

brew info juvix

Linux x86_64

A binary executable is available on the Juvix release page.

Building Juvix from source

To install Juvix from source you must clone the Github repository. Then Juvix can be installed with the following commands. We assume you have Stack installed.

git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install

On MacOS you can alternatively run the following command for Homebrew. The flag --HEAD used below is optional, use it to build the latest version of Juvix in the main branch on Github.

brew install --build-from-source --HEAD juvix --verbose

Quick Start

After installation run juvix --help to see the list of commands available. See CLI usage examples for descriptions of common tasks.

Run Juvix doctor to check your system setup:

juvix doctor

The Hello World example

This is the Juvix source code of the traditional Hello World program.

-- HelloWorld.juvix
module HelloWorld;

open import Stdlib.Prelude;

main : IO;
main ≔ putStrLn "hello world!";

end;

To compile and run a binary generated by Juvix, save the source code to a file called HelloWorld.juvix and run the following command from the directory containing it:

juvix compile HelloWorld.juvix
./HelloWorld

You should see the output: hello world!

The source code can also be compiled to a WebAssembly binary. This requires some additional setup. See Installing dependencies in the documentation for more information. You can also run juvix doctor to check your setup.

juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasm

The Juvix programming language

Juvix allows us to write programs with a high degree of assurance. The Juvix compiler runs several static analyses during the compilation phase to guarantee no runtime errors. Analyses permormed during this phase include scope, termination, arity, and type checkiqng. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors.

Some of the language features in Juvix include:

  • unicode syntax
  • parametric polymorphism
  • inductive and parametric data types
  • higher-order functions
  • implicit arguments
  • holes in expressions
  • axioms for non-computable terms

Additionally, the foreign and compile blocks syntax enable developers to compile a program to different backends including the C language. The Juvix module system further permits splitting programs into several modules to build libraries which can be later documented by generating HTML files based on the codebase, see for example, the Juvix standard library's website. For futher details, please refer to the Juvix book which includes our latest updates.

Coming soon

For the language:

  • lambda expressions
  • let expressions
  • tail call optimization
  • inference for mutually recursive functions
  • compilation to circuits
  • coverage checking (i.e. exhaustiveness and useless clauses)

For the compiler:

  • Init command
  • Better documentation tool: juvix doc MyFile.juvix

Community

We would love to hear what you think of Juvix! Join us on the Anoma Discord.