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/codespaces/new?hide_repo_select=true&ref=main&repo=455254004">
<img height="20pt" alt="Open the Juvix Standard Lib in Github Codespace" src="https://github.com/codespaces/badge.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/images/tara-seating.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 [[https://webassembly.org/][WebAssembly]], 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, the =juvix=
command line tool, the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Github Codespace]], and the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Standard Lib Codespace]]. However, we recommend using the =juvix-mode= in [[https://docs.juvix.org/reference/tooling/emacs.html][Emacs]] or the
plugin in [[https://github.com/anoma/vscode-juvix][VSCode]].

** Quick start

See [[https://docs.juvix.org/quick-start.html][Quick start]] to start with Juvix.

** The Juvix programming language

Juvix provides a high degree of assurance. The Juvix compiler runs
several static analyses which guarantee the absence of runtime
errors. Analyses performed include termination, arity, and type
checking. As a result, functional programs, especially validity
predicates, can be written with greater confidence in their
correctness.

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

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 further details, please refer to
[[https://anoma.github.io/juvix/][the Juvix book]] which includes our [[https://anoma.github.io/juvix/changelog.html][latest updates]].

** Community

Join us on our [[https://discord.gg/PfaaFVErHt][Discord server]]!

Juvix is part of a bigger effort called [[https://anoma.net/][Anoma]].
Anoma is an intent-centric, privacy-preserving protocol for decentralized counterparty discovery, solving, and multi-chain atomic settlement.
Join the [[https://anoma.net/community][Anoma project]].