The Emergence of Smart Contract Languages

Solidity, Vision and Roadmap

Dr. Gavin Wood and Dr. Christian Reitwiessner present the vision and roadmap of Solidity, the smart contract programming language.

Towards safer languages for smart contracts

Jack Pettersson and Robert Edström present Chalmers University of Technology, Sweden present on a dependantly typed functional language for smart contracts.

Designs for the L4 Contract Programming Language Based on Deontic Modal Logic

We propose the creation of a domain-specific-language (DSL) for (smart) contracts are consistent, correct, and complete. Our DSL, L4, doesn’t simply fill templates, it fulfills the Curry–Howard correspondence between computer programs and mathematical proofs, i.e., what functional languages do for the 𝜆-calculus, the DSL will do for the deontic modal μ-calculus. This means the DSL natively expresses obligations, permissions, prohibitions, and other contractual concepts in a way that computers can easily reason about. The compiler will be responsible for static analysis of the contracts and automated detection of several classes of errors, including: inconsistency, inompleteness, goal satisfaction, and policy compliance. Functional languages are well-suited for this kind of formal verification, and we developing L4 in Haskell. L4 derives from the academic literature on contract formalization, everything is opensource and we invite feature requests and contributors to define and create what will become "SQL for contracts".

New and future Features of Solidity

Update on how Solidity evolved in the recent months also showcasing features of Solidity in general and giving a roadmap for the future.

Solidity for Dummies

We will explore the basics of the Solidity contract language using examples.

Babbage: A mechanical smart contract language

In textual programming languages it is often almost impossible to see how different parts interact and fit together. Babbage is a visual programming language that consists of simple mechanical parts that aims to be understandable even by untrained people. Since interacting components have to be physically close, modularity is already guaranteed by design. The goal of Babbage is not to make it easy to create smart contracts, but to make it possible to create smart contracts whose functionality is easy to explain and understand.

Flexibility in Solidity

This talk presents latest updates and upcoming features of the Solidity language. Improvements in the code generator will greatly improve maintainability in the future. Furthermore, the next iteration of formal verification tools which will soon be a built-in component that helps you write safer smart contracts.

Intro to Solidity 2017 Edition

Hudson Jameson gives their talk titled, "Intro to Solidity 2017 Edition"

Introducing Rholang!

A correct-by-construction concurrent smart contracting language. We give a basic introduction and show a translation of ERC 20 token contract into Rholang.

Julia – IR for Ethereum Contracts

Brief introduction to Julia, a new intermediate language to be used in the Solidity compiler. It reduces the complexity of the compiler, helps in auditing contracts and makes supporting multiple VMs, such as EVM 1.5 and eWASM, possible.

AxLang: Compiling Scala to EVM Bytecode for Secure and Reliable Ethereum Smart Contracts

We present AxLang Backend: a compiler framework for verifiable Ethereum smart contracts, and Axoni’s first step toward releasing an open source full-stack Scala compiler for the Ethereum Virtual Machine (EVM). AxLang Backend significantly improves the ability to optimize, analyze, and verify/audit smart contracts through a standard intermediate representation (IR), a compiler norm that hasn’t previously been used by EVM compilers. Additionally, AxLang Backend can be used by other compilers to target the EVM in a more efficient manner. AxLang Backend consists of four main features: a clean, minimal intermediate language (IL) that serves as an effective compiler target as well as a human readable/writable languagea standard three-address code IR that is convertible to a static single assignment (SSA) form, as is common in widely-used general purpose compiler frameworksa retargetable code-generation module that converts IR into the desired executable codea decompiler that constructs the above IR from Ethereum bytecode produced by other compilers like Solidity. Axoni is developing AxLang because the ability to write verifiable smart contracts is critical to our clients' broad adoption of this technology. AxLang Backend is the underlying structure that makes it possible for AxLang and other high-level languages to efficiently target the EVM.

Less Gas, More Fun: Optimising Smart Contracts through Yul

Due to the relative simplicity of the Ethereum Virtual Machine, it is possible to perform heavy analyses in order to optimize bytecode. The jump operations are a main obstacle for this, because they might require a preservation of all basic blocks in the worst case. To overcome this, Solidity's new optimizer operates on an intermediate language called Yul, which is close to EVM bytecode (and also wasm) but abstracts jump operations through real function calls. Each of the many optimizing operations are simple local equivalence transforms whose effects can be inspected at any time and which in combination should be both more reliable and efficient than the classic optimizer.

Updates from the Solidity Team

In this talk we will give an overview of what the Solidity team has worked on in 2017/2018 and what our plans our for the next year. It will cover features, challenges and plans.

Yul - Intermediate language for Ethereum

This talk will give an introduction to Yul, the intermediate language developed by the Solidity team. We'll go through the motivation, design decisions and progress of implementation. Yul is designed to have multiple targets, EVM and ewasm, and support multiple languages as a frontend. We'll touch on languages using it (Flint, LLL) and what is ahead in order to support it in Solidity.

An EVM-based formal Rules Language

Smart contracts are immutable programs on the blockchain. They are automatically executed based on pre-defined rules. However, complex and inferencing rules could be extremely difficult to program, test, and validate, using standard programming languages like Solidity. The long sequences of highly nested and intersecting IF / THEN statements are fragile and error-prone. The problem is compounded by the need to frequently change rules based on business requirements. Enterprise software developers have long relied on Business Rules Engines (BREs) to solve this problem. BREs allow business analysts to write transactional (state changing) programs in a specialized programming language called formal rules language, which can be generated by graphical user interfaces. BREs automatically evaluate, re-evaluate, and execute those rules. They have been proven successful in traditional financial services. The Open Source Lity project developed extensions to Solidity so that the EVM could support BRE for smart contracts. In this presentation, I will discuss the benefits and use cases of rules language and engine for smart contracts especially in the context of financial services and e-commerce applications. I will further describe how the rules language extension for Solidity, modeled after Drools,  is designed and implemented, including compiler and runtime support.

Japanese, Human-Readable Smart Contracts

This workshop invites native or fluent Japanese speakers to create a Japanese-based smart contract language to create Ethereum smart contracts with that can be read by anyone who understands Japanese, and deployed directly to the Ethereum mainnet. Speakers of other languages who are interested in facilitating a Lexon variant based on their language are also invited to understand the process of adaption. The attempt is based on the Open Source, human-readable smart contract language Lexon that is a subset of natural English. This workshop is a hackathon-like event where the Lexon compiler source code and grammar is altered to see if a Japanese version of Lexon is possible. Coding skills are NOT required from participants. Lawyers and impact-oriented participants are highly welcome. Only one or two programmers — likely the tutor — will be working on code. The actual work will be for the audience to understand how the Lexon grammar is structured and to propose what has to be changed to make it work with Japanese. The result may be a working Lexon compiler for smart contracts written in Japanese, that anyone who can read Japanese can understand, and that can be compiled and run on the Ethereum main- and testnet immediately. This is possible because the Lexon grammar is relatively concise and changes to it can be made in a straight forward way that could lead to immediate results. At the least some experimental output should be achieved from an alpha version of a Japanese Lexon compiler. This is a different proposal from the workshop that teaches people how to write human-readable smart contracts in English. This Workshop is complementary, hands-on research part to the proposed 20-minute session about Human-Readable Smart Contracts. It will allow participants to shape the way forward for the project. (For your convenience, the following is a repeat from the complementary 20-minute session application that focusses on reading and the science behind it. 'Human-readable' smart contracts expand the audience of people who can read smart contracts by a thousand times. They democratize them beyond the ranks of developers and provide a means for expert validation, human debate and consensus. Lexon is a new type of program language that can be read by anyone without any preparation, made to create smart contracts that run on the Ethereum mainnet. It has been built from the ground up, over the course of two years, to allow lawyers and non-programmer experts to understand first-hand what a smart contract means. The result turns out to be enlightening for any community that wishes to allow their non-technical members to read for themselves what its DAO or smart contract code actually means. Turns out that's everyone except re-centralizing start ups. LEX Escrow Contract. “Payer” is a person. “Payee” is a person. “Arbiter” is a person. “Fee” is an amount. The Payer pays an Amount into escrow, appoints the Payee, appoints the Arbiter, and also fixes the Fee. CLAUSE: Pay Out. The Arbiter may pay from escrow the Fee to themselves, and afterwards pay the remainder of the escrow to the Payee. CLAUSE: Pay Back. The Arbiter may pay from escrow the Fee to themselves, and afterwards return the remainder of the escrow to the Payer. The enclosed paper draft explains the concept in-depth and has longer examples. Lexon is an Open Source project by the Lexon Foundation. It was created by the presenter and implemented by Marcelo Alaniz, Nicolas Guzzo and him.

RADON: a domain-specific language for oracles

Oracles are bound to bridge the gap—or abyss—between the realm of smart contracts and data coming from outside the blockchain. But, at the end of the day, achieving such ambitious goal boils down to removing the inherent indeterminism of real world events by aggregating, filtering and reducing multiple data points into a single one in a predictable way. This is no easy task—even more in the case of decentralized oracles. In this talk we will introduce RADON: a domain-specific language that provides a new ontology and semantics to enable smart contract developers to define how external data will be retrieved, aggregated, filtered, reduced and reported to their contracts. In a learn-by-doing manner, we will reflect on the challenges that we faced and the quirky, wicked and hidden incentives that can be accidentally introduced by poorly constructed queries. Finally, we will also demonstrate relevant tooling for ergonomically creating and troubleshooting oracle queries within the context of existing Solidity projects.

Yul, eWasm, Solidity: Progress and Future Plans

Over the last months, the Yul language has matured and proved its flexibility. The Solidity team has implemented an optimizer and an eWasm dialect and is now full steam working on rewriting the Solidity code generator to produce Yul code to replace sequences of EVM instructions.The Yul optimizer now matches the old EVM optimizer and already surpasses it with features like function inlining and cross-function optimization. This is also the main reason why the new code generator can be written in a super-modular way. Furthermore, it can equally operate on EVM- and eWasm-flavoured Yul code, which is important to cope with the 256- to 64-bit translation.Through this, the Solidity compiler can now output eWasm code, which makes efficient use of 64 bit types. Furthermore, the new code generator includes automated overflow checks everywhere, again something that would have destroyed the old optimizer. Future work:We plan to use a more intricate formal system to remove redundant operations and checks based on range-relations between variables. The introduction of memory area types will help optimizing memory allocation. Finally, a super-optimizer could prove useful, since it is worth spending extra time on compilation to save gas.