Try   HackMD

Hello potential PLT-research collaborator!

Rumour has it that you, a PL researcher, is interested in joint research with the Ethereum Foundation in developing new programming languages for writing Ethereum programs. Ever felt annoyed when industry doesn't listen to your hard-won PL wisdom? Ethereum aims to be the exception and, whenever possible, follow best practices in step with modern academic PL theory.

When it comes to PLT, we at Ethereum have convinced ourselves that, luckily, our desire for better smart-contract language(s) has substantial overlap with what PLT people already think about. So instead of growing our own PLT specialists, we prefer to collaborate with existing PLT people–-maybe you? Possible outputs from our collaboration are: peer-reviewed academic papers, technical reports, and/or implementations (prototypes as well as production-ready).

Ethereum is a suitable domain for implementing theoretically modern languages because:

  • Ethereum has few legacy requirements to support.
  • Ethereum developers already accept that blockchain programming is a "new paradigm" and are thus willing to learn and adopt new best practices.
  • Our bugs are bad. Like, really bad. For example, a single bug once resulted in >60M loss. As Ethereum grows, our bugs are only going to get worse, and we wish to better protect Ethereum developers using rigorous PLT.

Why would you want to work on this?

  • Designing the development stack of the global sky-computer is awesome.
  • This is an opportunity to mainstream your personal PL ideologies.
  • Your language specification could result in a flagship language underpinning Ethereum's growing >25 billion dollar ecosystem (not bad for a three year old project!).
  • If your research is especially aligned with Foundation interests, there's even funding for stipends to graduate students/postdocs.

The problem

Ethereum is a blockchain-based platform where users upload programs (called "smart contracts", "autonomous contracts", or "Dapps") to be executed by a globally viewable, bullet-proof, transparent, world computer. Unfortunately, dapp developers sometimes upload dapps with bugs. Then due to the transparent globally-readable nature of blockchains, this makes their dapps easy pickings for attackers to drain their stored ether (currency). We are seeking DSLs that permit extensive compile-time checks against common dapp bugs.

Goal: We wish to create a DSL that helps devs write short, simple, safe dapps, with the expectation that these techniques can later be scaled to more complex applications. Proposed properties for an improved dapp DSL are:

  • Amenable to Formal Verification techniques
    Particularly, these three properties for faciliating amendability to formal verification:
  • Eager-evaluation / "call-by-value" (simpler mental model for devs)
  • Polymorphism (for better developer experience)
  • Ideally, the ability to call-out to unverified code (calling other functions/dapps that aren't written in our language).
  • At some undetermined day in the future, we'd like to support Refinement (but not Dependent) Types.

What do we want the DSL to do that prior DSLs cannot?

  • Formal verification of common bugs.

Common dapp use-cases

When designing a DSL, there's always a question of what capabilities to make front and center. Although dapps are rather diverse, there are common Ethereum design patterns, often in the financial (e.g., receiving and sending ether, multi-signature transactions) and cryptographic domains (e.g., verifying signatures).

To get a broader view of the Dapp ecosystem, see these listings:

Common dapp bugs

On formal verification of dapps

Current High-level-languages (HLLs) for Ethereum

  • LLL - a Low-Level Lisp like language (largely deprecated).
  • Serpent - an early python like language (largely deprecated).
  • Solidity - the defacto standard for modern Ethereum development. Resembles Javascript. [Examples]
  • Functional Solidity - an experimental re-rendition of solidity as a functional language.
  • Viper - an experimental decidable language that resembles Python. [Examples]

Related languages

Appendix

Current developer user-experience

Ethereum has several handy developer tools. Most notably, these are:

If your language becomes popular, we would probably extend one of these existing IDEs to support your language and its various safety-checking.

People at the Foundation to chat PLT with:

Relative to other areas, the Foundation is weaker in PLT. But if you want to talk to people, we suggest:

On Turing completeness and the Etherem Virtual Machine (EVM)

Some of the cryptoeconomic community think it is immensely unwise for the EVM to be Turing complete. We disagree, and we prefer to give developers the full capabilities of Turing-Completeness. Then each developer can decide for zerself how much safety ze needs. If a developer wants more safety, ze can compile from an arbitrary Turing-incomplete language into the Turing-complete EVM.

On verifying compilers to EVM

As-is, the Ethereum Foundation is more interested in verifying properties of dapps than verifying compiler to EVM. We feel this way because the current EVM will eventually be replaced and we don't want you to spend your labor verifying something that will later be discarded. However, all future versions of the EVM will be Turing Complete.

However, if verified compilers are your thing, these will get you started:

On non-interference properties of Moon-lang

Moon-lang is designed so that imported libraries cannot do harm (like accessing a private key that's accessible in the main program). It would be nice to have a proof (at least on paper) around this requirement.

Last changed by 
 
Virgil Griffith
Internet Man of Mystery.
0
1289
Published on HackMD