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

Re: [tlaplus] Re: Ethereum Heist

Thanks for the clarification.

That is pretty much what I figured. My thinking was that the contract language could be something like TLA+ and then when the contract is executed (by some external implementation language) the terms specified by the TLA+ spec could be used to "validate" the contract's execution by said external implementation. Or maybe a contract could include a TLA+ spec in *addition* to the contract's Ethereum code to be used as a sanity check on the code and the before/after state. This probably doesn't make any sense and is applying TLA+ where it doesn't belong... just an incomplete train of thought... nevermind :-\


On Mon, Jul 11, 2016 at 9:16 PM, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:
TLA+ can specify unambiguously the full contract terms, their pre- and post-conditions, the bytecode VM and anything else you may want to know about Ethereum code. What it cannot do is implement any of it, because it's not a programming language... To a total newbie, I'd say think about TLA+ as a software simulation system, where you can simulate both your code and anything about the environment at any level of detail as you care to know. But instead of only running specific simulations, you can ask questions like "is this property always preserved?", "can this ever happen?" 

But you can't compile the simulation nor have the simulation interact with the outside world. It is a design and investigation tool that helps you build and understand software. This is why it can be especially suitable for Ethereum -- not as a replacement to anything, but precisely because everything is already built. TLA+ helps you write and understand programs regardless of the implementation language you choose.


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/uCcycpSzbZ4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

"Whatever you can do, or dream you can do, begin it. Boldness has genius, power, and magic in it. Begin it now." - Goethe