# Hello potential PLT-research collaborator!
Rumour has it that _you_, a PL researcher, is interested in _joint research_ with the [Ethereum Foundation](https://ethereum.org) in developing _new programming languages_ for writing [Ethereum](https://www.youtube.com/watch?v=j23HnORQXvs) 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](http://www.coindesk.com/dao-attacked-code-issue-leads-60-million-ether-theft/) 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](https://www.smbc-comics.com/?id=2088).
* 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](https://coinmarketcap.com/currencies/ethereum/) 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](http://truffleframework.com/tutorials/ethereum-overview) 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](http://vessenes.com/ethereum-contracts-are-going-to-be-candy-for-hackers/) 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:
* [Statically typed](https://www.sitepoint.com/typing-versus-dynamic-typing/), and [Strongly typed](https://en.wikipedia.org/wiki/Strong_and_weak_typing)
* A Turing-incomplete [decidable language](https://en.wikipedia.org/wiki/Recursive_language)
* A declarative language (but doesn't need to be a [total functional language](https://en.m.wikipedia.org/wiki/Total_functional_programming))
* 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](https://solidity.readthedocs.io/en/develop/common-patterns.html), 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:
* [Dapps listing](https://dapps.ethercasts.com/)
* Github's [list of Solidity repos](https://github.com/search?utf8=%E2%9C%93&q=topic%3Asolidity&type=Repositories)
* [Raw listing](https://etherscan.io/contractsVerified) from the ethereum blockchain of applications that provide both their sourecode as well as their bytecode
## Common dapp bugs
- [Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab](https://eprint.iacr.org/2015/460.pdf)
- [Ethereum Contract Security Techniques and Tips](https://github.com/ethereum/wiki/wiki/Safety)
- [Thinking About Smart Contract Security](https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/)
- [A survey of attacks on Ethereum smart contracts](https://eprint.iacr.org/2016/1007.pdf) see the attacks listed in the "Solidity" section.
- [Solidity security considerations](https://solidity.readthedocs.io/en/develop/security-considerations.html)
- Novice app writers often have a bug in their function that returns their ether. This makes it so any ether disposited into the contract becomes unretrievable.
## On formal verification of dapps
- [Writing smart contracts in Idris](https://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf)
- [Short Paper: Formal Verification of Smart Contracts](https://www.cs.umd.edu/~aseem/solidetherplas.pdf)
- [Oyente](https://github.com/melonproject/oyente), a vulnerability scanner for dapps [[pdf](https://eprint.iacr.org/2016/633.pdf)]
## Current High-level-languages (HLLs) for Ethereum
- [LLL](https://media.consensys.net/an-introduction-to-lll-for-ethereum-smart-contract-development-e26e38ea6c23) - a Low-Level Lisp like language (largely deprecated).
- [Serpent](https://github.com/ethereum/wiki/wiki/Serpent) - an early python like language (largely deprecated).
- [Functional Solidity](https://github.com/raineorshine/functional-solidity-language) - an experimental re-rendition of solidity as a functional language.
- [Viper](https://github.com/ethereum/viper) - an experimental decidable language that resembles Python. [[Examples](https://github.com/ethereum/viper#code-example)]
- [Composing contrats: an adventure in finanial engineering](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/contracts-icfp.pdf)
- [Hammurabi Project](https://github.com/mpoulshock/HammurabiProject) in Wolfram Language
## Current developer user-experience
Ethereum has several handy developer tools. Most notably, these are:
* [Truffle](http://truffleframework.com/) - the most popular IDE
* [Remix](https://ethereum.github.io/browser-solidity/) - a brower-based IDE
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:
* [Christian Reitwießner](mailto:[email protected]) (Solidity)
* [Vitalik Buterin](mailto:[email protected]) (Viper)
* [Virgil Griffith](mailto:[email protected]) (misc)
* [Yoichi Hirai](mailto:[email protected]) (Bamboo, or fancy propositional logics)
## On Turing completeness and the Etherem Virtual Machine (EVM)
Some of the cryptoeconomic community think it is [immensely unwise](https://steemit.com/crypto-news/@herzmeister/ethereum-must-drop-turing-completeness-or-it-will-fail) 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:
- [Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant](http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf)
- [Optimizing compilers to EVM](https://arxiv.org/pdf/1703.03994.pdf)
## On non-interference properties of Moon-lang
[Moon-lang](https://github.com/ethereum/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.