Juvix

[awacate]

After many months of R&D and continuous progress on the Juvix project, starting today we will post more updates, interesting reads on the project motivations, design and research.

Here’s the list of articles:

• The Why of Juvix Part I (teaser): https://medium.com/cryptium-research/the-why-of-juvix-part-1-on-the-design-of-smart-contract-languages-69071ece2bc
• The Why of Juvix Part I (full article): https://research.cryptium.ch/the-why-of-juvix-part-1-on-the-design-of-smart-contract-languages/

More resources:

• Repository: https://github.com/cryptiumlabs/juvix
• Language Reference: https://github.com/cryptiumlabs/juvix/blob/develop/doc/reference/language-reference.pdf

[mootjes]

Interesting but how does it compare to Michelson, e.g. in terms of readability

• readability, ease to write
• ease to formally verify
• security

Thanks.

[cwgoes]

Juvix is not (directly) an alternative to Michelson but rather a higher-level language which will be able to target Michelson (compile to it). Should Tezos add support for other execution environments such as WebAssembly in the future, Juvix will be able to target those as well without much difficulty. The frontend language will look a lot like Haskell or ML, with variables, functions, closures, user-defined algebraic data types, etc.

Juvix has dependent types, which allow you to express properties of terms in the language itself (by defining a type which captures the property), and prove those properties by inhabiting those types. We think that dependent types will facilitate easier formal verification because a separate tool is not required and because the proofs can be written directly in the higher-level language & more easily capture the semantics which the programmer cares about (e.g. conservation of supply for a token).

The language is still a work-in-progress right now, and we don’t recommmend using it for any actual contracts yet, but we expect it will be ready for initial use later this year.