Morley for Tezos
Morley was the first tool we completed for Tezos when we started our collaboration with Tocqueville Group.
Brief description
Tezos is an open-source project, and one of the biggest concerns of its founders was the lack of a convenient developer environment. To promote the usage of Tezos, increase its adoption, and develop its ecosystem, more effective tools needed to be made.
Tezos Foundation was looking for an expert team that could offer constructive improvements. Serokell had already completed several cryptocurrency projects in the past and could bring their expertise to the table.
Goals of the project:
Implement the Michelson typechecker and interpreter.
Invent a solution to test Michelson contracts conveniently.
Create new tools that make smart contract development easier.
MICHELSON & MORLEY
Tezos uses its own stack-based language – Michelson. While this language allows for formal verification of smart contracts and, therefore, is useful, it lacks some functionality. To solve that, we created Morley.
Morley consists of a set of tools and libraries that make writing smart contracts in Michelson pleasant and productive. It has data types representing everything present in Michelson, an implementation of the Michelson typechecker and interpreter, and a testing framework. Morley implements a dialect of Michelson that we call the Morley language.
Deliverables:
Strongly typed Michelson type system in Haskell. It serves as the basis for everything else in Morley.
Michelson typechecker and interpreter. The interpreter can run in an emulated environment.
Testing framework for Michelson contracts that can run either in an emulated environment or on the reference implementation of Tezos.
Some extensions to the Michelson language that make development in a low-level language like Michelson more convenient.
Challenges for developers
Tezos is not as mature as Bitcoin and Ethereum, and Michelson is a rather new language. Consequently, it is not that stable and "battle-tested". Due to this instability, some things kept changing, so we had to introduce massive changes in our codebase to account for changes.
Another technical challenge was to embed the Michelson type system into the Haskell type system. While dependent types would have greatly helped us, they are not yet present in modern Haskell. Hence, we had to resort to using GADTs and singletons. In the end, we managed to come up with Haskell data types representing well-typed Michelson contracts.
Result
