mirror of
https://github.com/anoma/juvix.git
synced 2024-12-12 14:28:08 +03:00
85 lines
3.9 KiB
Org Mode
85 lines
3.9 KiB
Org Mode
* 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/tooling/emacs-mode.html][Emacs]] or the
|
|
plugin in [[https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode][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/waYhQ2Qr][Discord server]]
|
|
|
|
This project is part of a bigger effort called [[https://anoma.net/][Anoma]].
|
|
Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination.
|
|
Join the [[https://anoma.net/community][Anoma project]].
|