[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 :-\