create account

Formal Verification of Smart Contracts and Wren by dana-edwards

View this thread on: hive.blogpeakd.comecency.com
· @dana-edwards · (edited)
$1,756.84
Formal Verification of Smart Contracts and Wren
![enter image description here](http://www.publicdomainpictures.net/pictures/150000/velka/business-world.jpg)

Recently Dan Larimer excitedly [announced](https://steemit.com/smartcontracts/@dantheman/could-wren-be-the-future-of-smart-contract-scripting-languages) 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](http://research.microsoft.com/en-us/um/people/nswamy/papers/solidether.pdf)" 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
👍  , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , and 301 others
properties (23)
authordana-edwards
permlinkformal-verification-of-smart-contracts-and-wren
categorysteem
json_metadata{"tags":["steem","steemit","crypto-news","tauchain","wren"],"image":["http://www.publicdomainpictures.net/pictures/150000/velka/business-world.jpg"]}
created2016-08-22 12:29:12
last_update2016-08-22 12:35:54
depth0
children16
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value1,597.498 HBD
curator_payout_value159.345 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length4,587
author_reputation353,623,611,191,427
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id933,640
net_rshares109,666,504,662,248
author_curate_reward""
vote details (365)
@dabaisha ·
Electronic money is a trend in the future
properties (22)
authordabaisha
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160823t101729443z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-23 10:18:06
last_update2016-08-23 10:18:06
depth1
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length41
author_reputation1,365,188,878,563
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id948,521
net_rshares0
@dantheman ·
$0.60
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.
👍  , , ,
properties (23)
authordantheman
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t144519936z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 14:45:18
last_update2016-08-22 14:45:18
depth1
children2
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.452 HBD
curator_payout_value0.146 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length288
author_reputation240,292,002,602,347
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id935,158
net_rshares893,108,024,318
author_curate_reward""
vote details (4)
@frk ·
Same, thats exactly how I feel about Tau also.
properties (22)
authorfrk
permlinkre-dantheman-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160823t130749276z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-23 13:07:39
last_update2016-08-23 13:07:39
depth2
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length46
author_reputation201,463,985,726
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id950,355
net_rshares0
@mark-waser ·
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.
properties (22)
authormark-waser
permlinkre-dantheman-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t155159362z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 15:52:03
last_update2016-08-22 15:52:03
depth2
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length305
author_reputation3,513,410,950,995
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id936,212
net_rshares0
@gekko ·
I'll definitely check it out! 8]
👍  
properties (23)
authorgekko
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160823t033105800z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-23 03:31:09
last_update2016-08-23 03:31:09
depth1
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length32
author_reputation1,185,517,433,922
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id945,529
net_rshares2,137,374,515
author_curate_reward""
vote details (1)
@knircky ·
Thank you for this post. I was not aware of this.
properties (22)
authorknircky
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160823t044847085z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-23 04:48:45
last_update2016-08-23 04:48:45
depth1
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length49
author_reputation212,905,587,244,262
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id946,116
net_rshares0
@mark-waser ·
$0.60
Possibly a stupid question but . . . . doesn't Rice's Theorem preclude Turing-complete language programs from being formally verified?
👍  , , , , , , , ,
properties (23)
authormark-waser
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t134705749z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 13:47:09
last_update2016-08-22 13:47:09
depth1
children5
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.456 HBD
curator_payout_value0.143 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length134
author_reputation3,513,410,950,995
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id934,476
net_rshares875,410,290,069
author_curate_reward""
vote details (9)
@dana-edwards · (edited)
$2.15
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://youtu.be/xbr9K-u0wmE
https://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06.pdf
👍  , , , , , , , , , , ,
properties (23)
authordana-edwards
permlinkre-mark-waser-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t152404717z
categorysteem
json_metadata{"tags":["steem"],"links":["https://youtu.be/xbr9K-u0wmE"]}
created2016-08-22 15:24:06
last_update2016-08-22 15:57:27
depth2
children3
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value1.619 HBD
curator_payout_value0.531 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length1,504
author_reputation353,623,611,191,427
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id935,762
net_rshares2,389,876,935,420
author_curate_reward""
vote details (12)
@mark-waser ·
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.
👍  
properties (23)
authormark-waser
permlinkre-dana-edwards-re-mark-waser-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t154850650z
categorysteem
json_metadata{"tags":["steem"],"links":["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."]}
created2016-08-22 15:48:54
last_update2016-08-22 15:48:54
depth3
children2
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length543
author_reputation3,513,410,950,995
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id936,153
net_rshares23,413,649,967
author_curate_reward""
vote details (1)
@dana-edwards · (edited)
Your question reveals how difficult it is to write correct programs and I found this video: https://www.youtube.com/watch?v=dWdy_AngDp0

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
1. http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/
properties (22)
authordana-edwards
permlinkre-mark-waser-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t153726854z
categorysteem
json_metadata{"tags":["steem"],"links":["https://www.youtube.com/watch?v=dWdy_AngDp0"]}
created2016-08-22 15:37:27
last_update2016-08-22 15:41:00
depth2
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length388
author_reputation353,623,611,191,427
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id935,973
net_rshares0
@matteo2016 ·
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.
properties (22)
authormatteo2016
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t163615051z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 16:36:15
last_update2016-08-22 16:36:15
depth1
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length155
author_reputation367,318,996,234
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id936,898
net_rshares0
@schro ·
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.
properties (22)
authorschro
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t123847280z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 12:38:48
last_update2016-08-22 12:38:48
depth1
children1
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length311
author_reputation5,439,139,781,025
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id933,761
net_rshares0
@dana-edwards · (edited)
$0.82
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.
👍  , , , ,
properties (23)
authordana-edwards
permlinkre-schro-re-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t124445240z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 12:44:45
last_update2016-08-22 12:45:51
depth2
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.617 HBD
curator_payout_value0.199 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length591
author_reputation353,623,611,191,427
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id933,827
net_rshares1,132,414,952,059
author_curate_reward""
vote details (5)
@stellabelle ·
Thank you for this information.
properties (22)
authorstellabelle
permlinkre-dana-edwards-formal-verification-of-smart-contracts-and-wren-20160822t205803974z
categorysteem
json_metadata{"tags":["steem"]}
created2016-08-22 20:58:03
last_update2016-08-22 20:58:03
depth1
children0
last_payout2016-09-22 18:41:27
cashout_time1969-12-31 23:59:59
total_payout_value0.000 HBD
curator_payout_value0.000 HBD
pending_payout_value0.000 HBD
promoted0.000 HBD
body_length31
author_reputation516,061,669,130,124
root_title"Formal Verification of Smart Contracts and Wren"
beneficiaries[]
max_accepted_payout1,000,000.000 HBD
percent_hbd10,000
post_id940,948
net_rshares0