State of the Languages

Project Updates
,
9

Thank you for following the latest in Tezos smart contract language development. We have fresh updates on all your favorite languages.

Let us know if you have:

  • feedback or suggestions
  • a language you would like to add

Recent development

Albert

In the past months the Albert compiler developers focused on testing. They are following a coverage-based methodology; the coverage infrastructure relies on an instrumentation by the bisect_ppx tool of the OCaml code extracted from Coq. A new feature has also been added to the language: the return instruction. The type of this instruction is return x : {x : a} -> a; a typical use-case of this instruction is in combination with iterators.

For example, doubling all elements in a list can now be done as follows:

def double : {n : nat} -> nat =
	two = 2;
	n = two * n;
	return ndef double_all : {l : list nat} -> {l : list nat} =
	l = map x in l do double{n=x} done

Archetype

The 1.1 version of Archetype was released last month. 1.1 completes the M1 milestone of the feature to transcode to archetype an existing contract: https://forum.tezosagora.org/t/archetype-1-1-and-fa1-2-contract/2110. Milestone M2 is on the way.

On the verification side, the Archetype team is working on the specification of contract entry failures. It will be possible to specify the state of the contract storage in case of a failure.

LIGO

The LIGO team:

  • completed and published the new VScode extension for LIGO. Check it out! VScode ligolang-publish.ligo-vscode
  • removed the dependency on the Tezos protocol from all LIGO compiler passes. This will make it easier to support targeting new protocols. It is also now possible for users to compile contracts which use new or experimental instructions, without any change to LIGO, by using the “Michelson insertion” feature and the --disable-michelson-typecheck option.
  • ported LIGO’s last compiler pass (the one which emits Michelson code) to Coq, with a nice extraction to OCaml. They are still integrating it with the rest of LIGO; for now there is only a proof of type preservation. They will prove some kind of semantic preservation and port more passes from OCaml to Coq.
  • worked on a LIGO test framework, which uses the LIGO interpreter. It allows us to test interoperation of contracts, assert for failure, and more
  • Alexandre Moine, a student pursuing a master’s degree in France, collaborated with the LIGO team to develop a linter for LIGO. The first version is available at https://github.com/nobrakal/lint_ligo/

The new linter supports the detection of:

  • deprecated built-ins
  • unused variables
  • code smells
  • mixed dialects for PascaLIGO (the LIGO documentation currently only features the so-called terse dialect, but some savvy programmers use the verbose one as well)

The linter is extensible in two ways:

  • by adding deprecated names
  • by contributing code patterns that match code smells. Hopefully the community will be interested in contributing more code patterns.

Technically, the underlying matching technique is based on the paper by Christian Rinderknecht and Nic Volanschi. Theory and Practice of Unparsed Patterns for Metacompilation. Science of Computer Programming, 75(3):85–105, March 2010. http://crinderknecht.free.fr/pub/scp2010.pdf

Michelson

No recent updates.

SmartPy

The SmartPy team worked recently on several subjects:

  • Chainlink support, in particular for the Chainlink Hackathon that is currently happening
  • elements towards a decompiler yielding further very nice optimizations in generated contracts including new “global” ones
  • migration of SmartPy.io to React (partially shipped)
  • some new features in the Michelson Editor https://SmartPy.io/dev/michelson.html which benefits from general improvements in the framework (better error reporting, instant typing, example generation, etc.)
  • improved documentation and examples
  • support of new test networks
  • experimental support for some new operations and types coming in future proposals

SCaml

The SCaml team just released SCaml 1.2.0. This supports Tezos Delphi protocol upgrade proposal, and newly supports scaml.ppx which can shift Tezos smart contract programming entirely within OCaml eco-system. With scaml.ppx SCaml smart contract code is embedded into OCaml executable, which generates the final Michelson code.

You can now use your favorite OCaml tools (Dune, Merlin, etc) freely to write smart contracts in SCaml!

Thank you for reading! Check back soon for our next update.

Eowyn on behalf of the LIGOlang team

2 Likes