Juvix

A more elegant language for a more civilized age

Smart contracts are security-critical, performance-sensitive, and bug-prone. Juvix utilizes recent advancements in type theory to allow 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 & execution.

Example

Smart Contract

This is a developer preview release of the Juvix smart contract language, supporting Michelson, the virtual machine utilized by the Tezos blockchain. This release supports standard functional syntax, full-spectrum dependent type checking, usage accounting, and compilation all the way to Michelson. A standard library is included containing Michelson's built-in primitive types and operations. This simple Juvix contract swaps out the previous storage value for whatever parameter is passed by the user calling the contract.

mod Const where

open Prelude
open Michelson

sig cons-pair : list operation -> nat -> pair (list operation) nat
let cons-pair = %Michelson.pair

sig nil : list operation
let nil = %Michelson.nil

sig main : pair nat nat -> pair (list operation) nat
let main = \ps -> cons-pair nil 10
Mascot

Stay tuned

Subscribe to our newsletter and receive the latest news and resources in your inbox.