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


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


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 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.


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.


eDSL in Haskell

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


eDSL in Haskell

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


Testing Michelson contracts.

Example based, property based tests.


Transpilation of contracts to SmartPy, LIGO.

Formal verification.