Michelson

Michelson is a domain specific programming language used to write smart contracts on the Tezos blockchain. The language allows users to prove the properties in their smart contracts through a formal verification process. The Michelson programming language is strongly typed, stack based and does not contain features such as polymorphism, closures, or named functions. A high-level programming called Liquidity can be written and compiled to the Michelson programming language. The implementation of the Michelson programming language is based around in OCaml GADT.