Compiling Juvix to Michelson

Juvix Is a dependently typed programming language inspired by Idris, F★, and Coq. Juvix is designed as a smart contract verification and execution language, where efficient compilation is key, as otherwise any inefficient compilation to the primitives of a virtual machine on a decentralized blockchain will result in extra funds spent in order to execute any given program (for more background on smart contract language design, see The Why of Juvix).

Juvix targets Tezos through its primitive script known as Michelson. Michelson is a peculiar language in that it is a typed stack based language in the lineage of Forth and Kitten. However, unlike these languages, Michelson lacks primitives to make standalone named functions.

Related Topics & Resources