Skip to content

An experimental programming language created by Heliax as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages.

License

anoma/juvix

main
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
January 5, 2023 17:48
January 31, 2023 18:31
January 31, 2023 18:31
January 5, 2023 17:48
January 31, 2023 18:31
November 3, 2022 09:38
January 18, 2023 10:23
January 19, 2023 15:44
January 18, 2023 10:23

Juvix

CI status pages-build-deployment LICENSE Open the Juvix Standard Lib in Github Codespace Juvix Mascot

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

This project is part of a bigger effort called Anoma. Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination. Join the Anoma project.

About

An experimental programming language created by Heliax as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages.

Topics

Resources

License

Stars

Watchers

Forks