Morley for Tezos

Morley was the first software project we created for Tezos when we started to work with Tocqueville Group.

Brief description

Tezos is an open-source platform, 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.
TQ group 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

The development of Morley helps Tezos teams to find any inconsistencies between the reference implementation and the documentation and so facilitates the debugging process. It removes barriers to entry and reduces the friction typically seen in the adoption of other blockchain platforms.

More Tezos projects

TezosLorenz&IndigoTZIP

Let’s Have a Chat

We would be happy to discuss your project and propose solutions.