by Christopher Goes, Marty Stumpf, Jeremy Ornelas, Andy Morris, Asher Manning
A high-level frontend syntax, dependent-linearly-typed core language

Juvix synthesises a high-level frontend syntax, dependent-linearly-typed core language, and low-level parallelisable optimally-reducing execution model into a single unified stack for writing formally verifiable, efficiently executable smart contracts which can be deployed to a variety of distributed ledgers.

Juvix’s compiler architecture is purpose-built from the ground up for the particular requirements and economic trade-offs of the smart contract use case — it prioritises behavioural verifiability, semantic precision, and output code efficiency over compilation speed, syntactical familiarity, and backwards compatibility with existing blockchain virtual machines.

Machine-assisted proof search, declarative deployment tooling, type & usage inference, and alternative spatiotemporal dataflow representations facilitate integration of low-developer-overhead property verification into the development process. An interchain abstraction layer representing ledgers as first-class objects enables seamless cross-chain programming and type-safe runtime reconfiguration

Information updated 07/18/20
View Comments