The entire and only possible point of a "smart contract" language is to bind two signed event structures ("blockchains") together. Thus these languages MUST be in terms of logical invariants of such structures, and to allow for universal quantification MUST be interactive proofs.
-
Show this thread
-
Do such languages need to be Turing complete or would a datalog-like language suffice? What about a TLA+ derived language? Clearly the implementation would need to be proved out. Turing completeness seems like overkill and a large attack surface.
2 replies 0 retweets 0 likes
Replying to @coopsource @sbelak
You will want to factor your datastructures and their properties such that you can have strong timely termination guarantees on your interactive proofs, to avoid issues like "You won one million dollar! Collect one dollar every week."
3:15 PM - 7 Jan 2018
0 replies
0 retweets
2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!