juvix/README.org

* MiniJuvix

#+begin_html
<a href="https://github.com/heliaxdev/minijuvix/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/heliaxdev/MiniJuvix/actions/workflows/ci.yml">
<img alt="CI status" src="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg" />
</a>
#+end_html

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


** Description

MiniJuvix is a programming language for writing efficient formally-verified
[[https://anoma.network/blog/validity-predicates/][validity predicates]], which can be deployed to various distributed ledgers. This
is software released for experimentation and research purposes only. No warranty
is provided or implied.

MiniJuvix addresses many issues that we have experienced while trying to
write and deploy decentralized applications present in the ecosystem of
smart-contracts:

- the difficulty of adequate program verification,
- the ceiling of compositional complexity,
- the illegibility of execution costs, and
- the lock-in to particular backends.

** Quick Start

To install MiniJuvix, you can download its sources using
[[http://git-scm.com/][Git]] from the
[[https://github.com/anoma/juvix.git][Github repository]]. Then, the
program can be downloaded and installed with the following commands. You
will need to have [[https://haskellstack.org][Stack]] installed.

#+begin_src shell
git clone https://github.com/heliaxdev/minijuvix.git
cd minijuvix
stack install
#+end_src

If the installation succeeds, you must be able to run the =minijuvix=
command from any location. To get the complete list of commands, please
run =minijuvix --help=.

- To test everything works correctly, you can run the following command. You will need to have [[https://emscripten.org][emscripten]] and [[https://wasmer.io][wasmer]] installed.

#+begin_src shell
stack test
#+end_src

** Usage Example

In the following example a MiniJuvix file is compiled using the C backend.  The result is compiled to WASM using [[https://emscripten.org][emscripten]] and then executed using  [[https://wasmer.io][wasmer]].

#+begin_src shell
cd tests/positive/MiniC/HelloWorld
minijuvix minic Input.mjuvix | emcc -x c - -o out.wasm && wasmer out.wasm
#+end_src

#+RESULTS:
: hello world!

** Other Documentation

[[docs/developer-tooling.org][Developer Tooling]]

** Community

We would love to hear what you think of MiniJuvix! Join us on
[[https://discord.gg/nsGaCZzJ][Discord]]