Abstract
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.
- Full Article on Metastate’s Research Blog
- This article was also shared on Metastate’s Medium Publication
Related Topics & Resources
- The Why of Juvix on Tezos Agora Forum
- Juvix’ Repository on GitHub
- More articles on PLT and Smart Contract R&D
