Competition Juvix - Glow-Lang/glow GitHub Wiki

Juvix is a programming language for Tezos smart contracts

Pros:

• It is a language integrated with a proof system, so you can write proven-correct programs.
• It was initially Tezos-focused, but now also targets LLVM and through it WASM as well as Michelson, and even Plonk zk-SNARKs.

Cons:

• Juvix developers seem to have no idea what are the interesting things to prove about contracts. But they do have an interesting framework for "validity predicates".
• Juvix has no notions about the adversarial aspect of interactions, that is central to Glow.
• Unlike Glow, Juvix doesn't currently seem to output client and server code.