# Compiling Juvix to Michelson **URL:** https://forum.tezosagora.org/t/compiling-juvix-to-michelson/1889 **Category:** Research and Development **Tags:** michelson **Created:** [May 8, 2020, 1:27pm UTC](https://forum.tezosagora.org/t/compiling-juvix-to-michelson/1889 "2020-05-08T13:27:16Z") **Posts on this page:** 1 **Page:** 1
### Author: ![metastate](https://forum.tezosagora.org/user_avatar/forum.tezosagora.org/metastate/32/349_2.png) [@metastate](https://forum.tezosagora.org/u/metastate) #### Post date: [May 8, 2020, 1:27pm UTC](https://forum.tezosagora.org/t/compiling-juvix-to-michelson/1889/1 "2020-05-08T13:27:16Z")
**Abstract** `Juvix` Is a dependently typed programming language inspired by [Idris](https://www.idris-lang.org/), [F★](https://www.fstar-lang.org/), and [Coq](https://coq.inria.fr/). 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](https://research.metastate.ch/the-why-of-juvix-part-1-on-the-design-of-smart-contract-languages/)). `Juvix` targets [Tezos](https://tezos.com/) through its primitive script known as [Michelson](https://michelson.org/). [Michelson](https://michelson.org/) is a peculiar language in that it is a typed stack based language in the lineage of [Forth](https://www.forth.com/forth/) and [Kitten](https://kittenlang.org/). However, unlike these languages, Michelson lacks primitives to make standalone named functions. - Full Article on [Metastate’s Research Blog](https://research.metastate.dev/juvix-compiling-juvix-to-michelson/) - This article was also shared on Metastate’s [Medium Publication](https://medium.com/metastatedev/juvix-compiling-juvix-to-michelson-c9d450d23fbd) **Related Topics & Resources** - [The Why of Juvix](https://forum.tezosagora.org/t/juvix/1550) on Tezos Agora Forum - [Juvix’ Repository on GitHub](https://github.com/cryptiumlabs/juvix) - [More articles on PLT and Smart Contract R&D](https://research.metastate.dev/tag/programming-language-theory/)