juvix/README.org

* Juvix

#+begin_html
<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>
#+end_html

#+begin_html
<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>
#+end_html

#+begin_html
<a href="https://github.com/anoma/juvix/tags">
<img alt="" src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases" />
</a>
#+end_html

#+begin_html
<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>
#+end_html

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


** Description

Juvix is a research programming language created by [[https://heliax.dev/][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 [[https://anoma.network/blog/validity-predicates/][validity predicates]] to the =C= language, which can be deployed to various distributed ledgers including [[https://anoma.net/][Anoma]].

The Juvix language and related tools are documented in [[https://anoma.github.io/juvix/][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 [[https://docs.juvix.org/tooling/emacs-mode.html][Emacs]] or the
plugin in [[https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode][VSCode]].

** [[https://github.com/anoma/juvix/tree/main/examples/milestone][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=.

- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]

The [[https://anoma.github.io/juvix-stdlib/][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 [[https://brew.sh][Homebrew]].

To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:

#+begin_src shell
brew tap anoma/juvix
#+end_src

To install Juvix, run:

#+begin_src shell
brew install juvix
#+end_src


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

#+begin_src shell
brew info juvix
#+end_src

*** Linux x86_64

A binary executable is available on the [[https://github.com/anoma/juvix/releases/latest][Juvix release page]].

*** Building Juvix from source

To install Juvix from source you must clone the [[https://github.com/anoma/juvix.git][Github repository]]. Then Juvix
can be installed with the following commands. We assume you have [[https://haskellstack.org][Stack]]
installed.

#+begin_src shell
git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install
#+end_src

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.

#+begin_src shell
brew install --build-from-source --HEAD juvix --verbose
#+end_src

**  Quick Start

After installation run =juvix --help= to see the list of commands available. See
[[https://docs.juvix.org/getting-started/quick-start.html#cli-usage-examples][CLI usage examples]] for descriptions of common tasks.

Run Juvix doctor to check your system setup:

#+begin_src shell
juvix doctor
#+end_src

*** The Hello World example

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

#+begin_src shell
-- HelloWorld.juvix
module HelloWorld;

open import Stdlib.Prelude;

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

end;
#+end_src

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:

#+begin_src shell
juvix compile HelloWorld.juvix
./HelloWorld
#+end_src

You should see the output: =hello world!=

The source code can also be compiled to a WebAssembly binary. This requires some
additional setup. See [[https://anoma.github.io/juvix/getting-started/dependencies.html][Installing dependencies]] in the documentation for more
information. You can also run =juvix doctor= to check your setup.

#+begin_src shell
juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasm
#+end_src

** 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, [[https://anoma.github.io/juvix-stdlib/][the Juvix
standard library's website]]. For futher details, please refer to
[[https://anoma.github.io/juvix/][the Juvix book]] which includes our
[[https://anoma.github.io/juvix/introduction/changelog.html][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
[[https://discord.gg/vEQappb7wG][the Anoma Discord]].