Tezos

Accounts

Implicit - non programmable, tagged to public key

Smart contract - programmable. Transaction can contain data, fail for reasons decided by michelson code. Address unique hash that depends on operation that created it. Address starts with KT1.

Both are indistinguishable.

Smart contract languages

Michelson

Stack based, strict static type checking. Values are immutable and garbage collected. types of input, output stack are fixed, monomorphic. Program is typechecked.

SmartPy

Embedded DSL in python. Users can write and implement test scenarios to test their smart-contracts.

Compiles to imperative, type inferred intermediate language called SmartML.

SmartML in turn compiles to Michelson.

LIGO

LIGO supports:

  • CameLIGO - OCaml inspired syntax
  • ReasonLIGO - functional Javascript-like syntax inspired by ReasonML
  • PascaLIGO - Pascal inspired syntax.

LIGO -> IR -> typecheck -> Michelson.

Morley framework

Collection of projects which build upon and complement each other.

Morley

Haskell framework for meta-programming Michelson smart contracts.

Morley (.mtz) - superset of Michelson, with simpler syntax, simple features.

Library with core Tezos, Michelson datatypes & tools for typechecking, interpreting, parsing and printing Michelson, Morley contracts.

Executable with commands for compiling and working with Morley and Michelson contracts, along with a REPL for interactively running instructions.

Lorentz

eDSL in Haskell

  • Expressive type system
  • type inference
  • Type safe
  • Reuse components as Haskell packages
  • Autogen docs

Indigo

eDSL in Haskell

  • imperative style programming, free you from manual stack management.

Cleveland

Testing Michelson contracts.

Example based, property based tests.

Archetype

Transpilation of contracts to SmartPy, LIGO.

Formal verification.

logo