Formal Verification of Smart Contracts and Wren
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
Possibly a stupid question but . . . . doesn't Rice's Theorem preclude Turing-complete language programs from being formally verified?
That is a very good question and it would take an entire blog post to answer it fully. Short answer is you don't formally verify the programming language, but you do verify the programs (Programs = Proofs). There are different methods of doing that and in the Ethereum example in the paper Solidity is translated into F* which is a functional programming language that makes formal verification a straight forward process. Programs can be formally verified by many different methods and my understanding of Rice Theorem is that certain problems are undecidable, but you can always determine when the finite program terminates, you can avoid infinite loops. With MSOL over graphs which appears to be state of the art, you can express any finite computer program. You have the benefit of a consistent logic MSOL and my understanding is that any software written under this logic ultimately is correct at the compiler level because formal verification could constrain unexpected behavior. But I will also say, because the ideas and papers are so new to me, I may not fully understand it, and Ohad himself may not fully understand it, because this is on the bleeding edge of what is possible. What we can do is simply research it together and blog about it but my current understanding is you can do formal verification but some problems remain undecidable due to Rice's Theorem.
References
https://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06.pdf
I would love to research it and blog about it together. I am very interested in getting into smart contracts and really do think that it would be an awesome doable project for the hackathon . . . . https://steemit.com/steemit/@mark-waser/less-than-hack-ether-camp-greater-than-a-4-week-virtual-hackathon-to-build-out-steem-tools-1st-prize-usd50-000.
I've been doing a lot of thinking about how much is required in terms of necessary hooks available from/provided by steem and how society-based escrow/bonding is most effectively performed.
Once there is a smart contract capability for Steem via sidechain then I think we will see a flood of smart contracts. Let's hope we get this smart contract functionality in an upcoming hard fork.
Clearly there is a lot of demand from developers for this functionality because you see so many apps so soon.
#hassan #rouhan #steven #spielberg
https://steemit.com/news/@cryptocurrency1/https-www-youtube-com-watch-v-iovkjhu7mfk
Your question reveals how difficult it is to write correct programs and I found this video:
The video seems to illustrates what your question leads to. So we can never fully know certain things and the video mentions reachability and Rice's Theorem.
Reference
To be clear, I like the idea of Tau. Like you said it is incomplete and you are ultimately relying on an implementation that could still be buggy. At some point I will have to dive into the Tau concepts.
I also think that not all smart contracts require the same level of security.
I think that you mean verifiability rather than security.
There will be an awesome market eventually for re-writing contracts for verifiability since -- while some languages certainly permit unverifiable contracts -- many, if not most, contracts written in those languages are/will be still verifiable.
Same, thats exactly how I feel about Tau also.
I'll definitely check it out! 8]
Interesting write up. I have only recently begun looking into the docs for Wren and i wasn't aware of Tau at all. But will keep an eye on the development of it now. Smart contracts are a very new area for me. So it's great to get other peoples perspective on some of the pro and cons as it were of the language.
Wren seems performance oriented. Tau is security oriented but will also be very high performing. Tau is more powerful but Wren is something which can be implemented immediately. Sometimes to expand on your momentum you can implement something immediately even though you might swap it out for something better later.
Steem (Graphene) is the highest performance blockchain architecture available. Steem can achieve mass adoption because it can scale and be fast, and Wren would allow Steem to leverage it's design advantages. Tau on the other hand is much more powerful but is not finished.
no competencies here, whatsover, but it's nice to get exposed to technical language and issue, anyhow. I might remember a term or two in my next tech read.
Thank you for this post. I was not aware of this.
Electronic money is a trend in the future