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.
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
Subscribe to our newsletter and receive the latest news and resources in your inbox.