1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-12 14:28:08 +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
janmasrovira 23f34403f5
Move substEnv to its own module (#1861)
The pretty printer for `Core` depends on `substEnv`, so it is convenient
to have it isolated so that it is possible to use ``ppTrace`` when
debugging functions in `Core.Utils` (or anything depending on it).
2023-02-22 19:21:41 +01:00
.devcontainer Add initial setup for codespaces (#1713) 2023-01-18 11:25:18 +01:00
.github Apply CI ghcup workaround to docs build (#1823) 2023-02-08 18:14:56 +00:00
app Add Geb Backend Evaluator with some extra subcommands (#1808) 2023-02-22 15:27:40 +01:00
assets Refactor html command with extra options (#1725) 2023-01-17 18:11:59 +01:00
bench Automatized benchmarks (#1673) 2023-01-05 17:48:26 +01:00
c-runtime String builtins (#1784) 2023-01-31 18:31:04 +01:00
docker Upgrade stack snapshot to use ghc-9.2.5 (#1621) 2022-12-02 10:04:56 +01:00
docs/org Documentation: update language reference (#1829) 2023-02-10 17:25:40 +01:00
examples Format examples (#1856) 2023-02-21 20:40:09 +01:00
gnuplot Automatized benchmarks (#1673) 2023-01-05 17:48:26 +01:00
juvix-stdlib@3a7d37febd Add Geb Backend Evaluator with some extra subcommands (#1808) 2023-02-22 15:27:40 +01:00
licenses Add Haddock and Agda licenses (#1506) 2022-09-06 09:30:01 +01:00
runtime String builtins (#1784) 2023-01-31 18:31:04 +01:00
src/Juvix Move substEnv to its own module (#1861) 2023-02-22 19:21:41 +01:00
test Add Geb Backend Evaluator with some extra subcommands (#1808) 2023-02-22 15:27:40 +01:00
tests Add Geb Backend Evaluator with some extra subcommands (#1808) 2023-02-22 15:27:40 +01:00
.clang-format Juvix C runtime (#1580) 2022-11-03 09:38:09 +01:00
.github_changelog_generator Update Changelog v0.2.3 🎉 2022-08-15 12:24:42 +02:00
.gitignore Automatized benchmarks (#1673) 2023-01-05 17:48:26 +01:00
.gitmodules Rename MiniJuvix to Juvix (#259) 2022-07-08 13:59:45 +02:00
.hlint.yaml Remove hlint from the CI and pre-commit config (#1759) 2023-01-24 13:55:12 +01:00
.pre-commit-config.yaml Update pre-commit (#1772) 2023-01-27 14:24:10 +00:00
.pre-commit-hooks.yaml Remove hlint from the CI and pre-commit config (#1759) 2023-01-24 13:55:12 +01:00
book.toml No run jobs after pr is closed/merged, docs only on pushes to main (#1779) 2023-01-27 19:01:25 +01:00
cabal.hie.yaml Automatized benchmarks (#1673) 2023-01-05 17:48:26 +01:00
cabal.project Update stack.yaml (#1734) 2023-01-18 10:23:14 +01:00
changelog.org Fix broken links and other improvements (#1761) 2023-01-24 17:21:35 +01:00
cntlines.sh Basic Geb integration (#1748) 2023-02-01 12:04:05 +01:00
LICENSE First commit, initial project template. 2021-09-26 18:59:51 +02:00
Makefile Add Geb Backend Evaluator with some extra subcommands (#1808) 2023-02-22 15:27:40 +01:00
package.yaml Bump up version to v0.2.9 2023-01-19 15:44:25 +01:00
README.org Update README.md Closes #1855 2023-02-22 18:00:51 +01:00
stack.hie.yaml Refactor hie.yaml and add entry in the readme (#1672) 2022-12-20 16:45:48 +01:00
stack.yaml Update stack.yaml (#1734) 2023-01-18 10:23:14 +01: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/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>

<a href="https://github.com/anoma/juvix"> <img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/images/tara-seating.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 WebAssembly, 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, the juvix command line tool, the Juvix Github Codespace, and the Juvix Standard Lib Codespace. However, we recommend using the juvix-mode in Emacs or the plugin in VSCode.

Quick start

See 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, the Juvix standard library's website. For further details, please refer to the Juvix book which includes our latest updates.

Community

Join us on our Discord server!

Juvix is part of a bigger effort called Anoma. Anoma is an intent-centric, privacy-preserving protocol for decentralized counterparty discovery, solving, and multi-chain atomic settlement. Join the Anoma project.