Formal Verification of Smart Contracts and Wren

enter image description here

Recently Dan Larimer excitedly announced Wren as a new scripting language for smart contracts. The language looks to be exceptionally efficient compared to other scripting languages. It has interesting properties and is deterministic. Wren has familiar looking syntax, similar to Javescript, C or C++, and this familiarity may make it easier to write smart contracts in Wren.

Implementation

Dan Larimer has proposed the idea of making a specific smart contracts side chain for Wren. Would doing it in this way preserve the design modularity of Steem? Based on my limited understanding of side chains, it would, but this needs to be clarified. It is my opinion that while Wren is an interesting and familiar high performance language, it's not the ideal language for smart contracts. I see Wren as a transient yet optional language to use until next generation languages Tau are available.

Wren vs Tau

Wren while impressive, and while we know a skilled programmer like Dan Larimer can write secure smart contracts, it's still relying on the bottle neck which requires absolute trust in the capabilities of the programmers. If it is possible to mess up then how will we deal with programmers who deliberately mess up as an act of sabotage? In order to trust Wren based on my understanding, we would need to rely on mandatory formal verification as a layer between the programmer and the execution of the smart contract. Wren has a particularly interesting feature to take note of called fibers and it reveals Wren is performance oriented:

Fibers are a key part of Wren. They form its execution model, its concurrency story, and take the place of exceptions in error handling. They are a bit like threads except they are cooperatively scheduled. That means Wren doesn't pause one fiber and switch to another until you tell it to. You don't have to worry about context switches at random times and all of the headaches those cause.

Considering Steem has the LMAX design, the high performance of the smart contracts is a potential edge when compared to the slow performing Ethereum smart contract design.

Tau currently is undergoing a bit of a redesign. In my future posts I will discuss it further but the current state of the art in terms of logic is called Monadic Second Order Logic (MSOL) and the new design for Tau has removed Martin Lof Type Theory in favor of Monadic Second Order Logic over Graphs. The point of Tau is that it is being designed from the ground up to be the ideal secure smart contract programming language for the minimal trust environment.

Formal Verification of Smart Contracts for EVM

A new paper was just released from Microsoft on formal verification of smart contracts titled: "Short Paper: Formal Verification of Smart Contracts" which outlines a method of integrating formal verification into Ethereum Smart Contracts by way of Solidity. It is in my opinion that formal verification should be mandatory for a Turing complete language if the intention is to write smart contracts which handle serious amounts of money, or are involved in the Internet of Things.

Conclusion

In my current opinion based on current knowledge, Steemit can utilize Wren. Steemit is not currently managing billions of dollars, or doing the Internet of Things, and Dan Larimer has a very good track record for writing secure software. Because Steem is so young, because there are few developers we would have to trust, and because of how Wren will be implemented, it's one of the better choices from the currently available options.

That said, I hope those who do choose to implement and use Wren, also follow the development of Tau. Because Tau is such a promising language, it could benefit Steem in the long term to swap out of Wren and into Tau if we get to the point where Tau is shown to work. In a situation where developers have a choice, a developer could choose today to write their smart contract in Wren, but do so in a way where it can easily be ported to Tau in the future if Tau becomes an option.

References
http://wren.io/getting-started.html
https://github.com/steemit/steem/issues/308
http://research.microsoft.com/en-us/um/people/nswamy/papers/solidether.pdf

H2
H3
H4
3 columns
2 columns
1 column
16 Comments