[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Ethereum Heist



What's unclear to me is that if TLA+ is the right tool?

It appears that what smart contracts need is not TLA, but an operational semantics for the language that smart contract provide?  Is TLA+ sufficient but not necessary?  That's my concern.  It seems that an operational semantics based on the language that the smart contracts provide would be necessary to ensure safety without restoring to something that TLA, that while may ensure correctness, might not be the proper fit for what needs to be proved.

- Christopher

On Tuesday, July 12, 2016 at 9:09:02 AM UTC+2, Ron Pressler wrote:
There is nothing magical about TLA+ as a language. Leslie Lamport is a well-known opponent of the trend of "thinking in languages" ("Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages."). TLA+ just has clear, well-understood and relatively standard mathematical semantics, and is a tool for rigorously reasoning about what programs do. Putting something like TLA+ into the Ethereum language for execution at runtime wouldn't currently make much sense for complexity reasons. Writing Ethereum specs in a language with built-in verification tools is a whole other matter, but as what is executed is bytecode anyway, you have no assurance that the code you're executing is the code you verified.

But yes, use TLA+ in addition to Ethereum code. A TLA+ spec is a verifiable blueprint; the code itself is the building. It is much more than a sanity-check, though. It is a verification of your design. 

In addition to verifying contract design in general, TLA+ can model the Ethereum VM itself, and could be used to verify compiled Ethereum contracts. The Ethereum VM seems to be pretty thoroughly specified and is not too big, so a formal TLA+ spec seems like a very feasible and worthwhile goal. But that's a somewhat different use of the tool, although some combination of the two may be interesting as well.

The real challenge is figuring out what safety properties you'd want to verify for a contract. That is a job for the Ethereum domain experts, economists, lawyers etc..

Ron