4 ms·

It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's eff

by buckie 9y ago

It's closest to the middle, assuming that you meant that you're stating the properties that you want to test. It does more than that, but at its base that's effectively how it works so it's close enough for a solid intuition. We're working on a paper about it now -- or at least a sub-paper in the clutch of papers that pertain to a public chain version -- that I'll link to when it's out (a couple weeks probably).

lomnakkus 9y ago
Oh. Dear? (I mean, I understand the pressures of academia, but... ridiculously bad timing, yeah?)
- Amanda343 9y ago
  I get paid over $95 per hour working from home with 2 kids at home. I never thought I'd be able to do it but my best friend earns over 10k a month doing this and she convinced me to try. The potential with this is endless. Heres what I've been doing, •••••••••>>https://is.gd/qKRnJt https://is.gd/qKRnJt
- deleted 9y ago
  [deleted]
- buckie 9y ago
  Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have? At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital). It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part. Also, not an academic (yet at least). Cofounder here: http://kadena.io http://kadena.io [1]: https://goldsilverbitcoin.com/jp-morgans-blockchain-researchers-discussed-ethereums-shortcomings-before-dao-hack/ https://goldsilverbitcoin.com/jp-morgans-blockchain-research...
  - Jabanga 9y ago
    >This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. I don't see any justification for this statement. The bug could easily have been discovered if there had been better auditing. That the auditing missed the bug doesn't prove that it's "practically impossible" to write secure code with Solidity. In any case, nothing is stopping you from porting your formally verifiable language to Ethereum. The EVM is not Solidity. In fact there is already a project underway to create a verifiable programming language for the EVM.
    - buckie 9y ago
      > That the auditing missed the bug doesn't prove... Honest question, what would be required in your opinion for before we start considering if the tool is at fault? I ask because, if you're of the opinion that it's never the tools fault then I'll never be able to justify my point of view. Which is fine, we can disagree. I'm all for massive experimentation in this area and thus need people who disagree with me to do research down the other lines. Also, it's not that I think it will always be practically impossible just that currently (and for the next several years at the very least) it is. We'd need way better tooling and the type of tooling needed is incredibly advanced stuff. We're not talking about a build system here, we're talking about formal verification which is one of the most advanced tools you can build. I can only think of one tool that can formally verify user generated code (cryptol) and even then it's only for a small subset of C/Java that applies to crypto work. It's not that you can't write safe solidity contracts today but that IMO an element of luck is required. You need to get the right auditors, have them do a good enough job, implement the logic a certain way instead of another and thus avoid a bug no one has thought about before, etc... When people's money is on the line, needing luck is terrifying. > nothing is stopping you from porting your formally verifiable language to Ethereum I wish this were true but it isn't. We spent months trying to see if there was a way that it would work because we would have preferred this approach. The EVM itself is stopping us (as well as the shape of the Eth blockchain but we could probably have worked around that problem). Pact is interpreted, so while we could make an EVM version technically it's practically unworkable -- there's nowhere near enough gas to run the interpreter. We couldn't compile directly to EVM either as the EVM just doesn't do enough[1] for you. It's closer to a 1980's era CPU ASM than a modern VM (like the JVM). Moreover, the Pact runtime does a lot of things for you (as a safety feature) that the EVM just doesn't have a notion of. Even then, while all of the Pact-compiled-to-EVM code would work and be safe, we couldn't protect it that code from EVM code that doesn't play by Pact's rules. Moreover, supporting all the extra things that Pact does for you would make it, again, run out of gas on EVM. This discussion is very similar to putting Ed25519 on the EVM. While you can technically implement it in EVM, it's just too gas-heavy. It's best to extend the EVM itself to do more. That's the thing about having the EVM be Turing-complete, it makes people think that "it can do anything and thus abstracts over the problem thus solving it." This is technically true but not practically true -- all you are doing is punting a huge number problems/required features (like dispatch and module loading) down the road for the language to figure out. In a gas-metered context, every feature the language adds because the EVM lacks it costs gas and thus makes a number of features impossible in practice. > In fact there is already a project underway to create a verifiable programming language for the EVM. Mind linking me to it? I collect references to smart contract languages at this point and haven't heard of this one. I know the people working on the EVM + solidity formal verification project personally (well some of them at least) and it's still years away. [1]: Great technical discussion about EVM here -- https://news.ycombinator.com/item?id=14689792 https://news.ycombinator.com/item?id=14689792

by buckie 9y ago

lomnakkus 9y ago

Oh. Dear? (I mean, I understand the pressures of academia, but... ridiculously bad timing, yeah?)

Amanda343 9y ago
I get paid over $95 per hour working from home with 2 kids at home. I never thought I'd be able to do it but my best friend earns over 10k a month doing this and she convinced me to try. The potential with this is endless. Heres what I've been doing, •••••••••>>https://is.gd/qKRnJt https://is.gd/qKRnJt
deleted 9y ago
[deleted]
buckie 9y ago
Why bad timing? This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. "One of the best Solidity devs" just failed to write a safe contract to the tune of a $30M exploit. Given that, what chance does anyone else have? At some point, it's time to blame the tool and not the user. Moreover, it's not like people didn't see this coming, myself included[1]. I mean, who really thought that basically taking JavaScript and swapping out the DOM for a bank account wasn't going to end badly? But then again, maybe I've spent too much time at in the SEC/finance where "move fast and break things" engineering gets you shown the door quite quickly. That mantra's fine for a number of domains but finance isn't one of them as one bug can bankrupt the company (see: knight capital). It really just underlines the need for a safer/better approach. Formal Verification has to be part of that story. A language that was designed with safety in mind has to be another part. Also, not an academic (yet at least). Cofounder here: http://kadena.io http://kadena.io [1]: https://goldsilverbitcoin.com/jp-morgans-blockchain-researchers-discussed-ethereums-shortcomings-before-dao-hack/ https://goldsilverbitcoin.com/jp-morgans-blockchain-research...
- Jabanga 9y ago
  >This is really just an example that while safe smart contracts are technically possible using Solidity/EVM, it's practically impossible. I don't see any justification for this statement. The bug could easily have been discovered if there had been better auditing. That the auditing missed the bug doesn't prove that it's "practically impossible" to write secure code with Solidity. In any case, nothing is stopping you from porting your formally verifiable language to Ethereum. The EVM is not Solidity. In fact there is already a project underway to create a verifiable programming language for the EVM.
  - buckie 9y ago
    > That the auditing missed the bug doesn't prove... Honest question, what would be required in your opinion for before we start considering if the tool is at fault? I ask because, if you're of the opinion that it's never the tools fault then I'll never be able to justify my point of view. Which is fine, we can disagree. I'm all for massive experimentation in this area and thus need people who disagree with me to do research down the other lines. Also, it's not that I think it will always be practically impossible just that currently (and for the next several years at the very least) it is. We'd need way better tooling and the type of tooling needed is incredibly advanced stuff. We're not talking about a build system here, we're talking about formal verification which is one of the most advanced tools you can build. I can only think of one tool that can formally verify user generated code (cryptol) and even then it's only for a small subset of C/Java that applies to crypto work. It's not that you can't write safe solidity contracts today but that IMO an element of luck is required. You need to get the right auditors, have them do a good enough job, implement the logic a certain way instead of another and thus avoid a bug no one has thought about before, etc... When people's money is on the line, needing luck is terrifying. > nothing is stopping you from porting your formally verifiable language to Ethereum I wish this were true but it isn't. We spent months trying to see if there was a way that it would work because we would have preferred this approach. The EVM itself is stopping us (as well as the shape of the Eth blockchain but we could probably have worked around that problem). Pact is interpreted, so while we could make an EVM version technically it's practically unworkable -- there's nowhere near enough gas to run the interpreter. We couldn't compile directly to EVM either as the EVM just doesn't do enough[1] for you. It's closer to a 1980's era CPU ASM than a modern VM (like the JVM). Moreover, the Pact runtime does a lot of things for you (as a safety feature) that the EVM just doesn't have a notion of. Even then, while all of the Pact-compiled-to-EVM code would work and be safe, we couldn't protect it that code from EVM code that doesn't play by Pact's rules. Moreover, supporting all the extra things that Pact does for you would make it, again, run out of gas on EVM. This discussion is very similar to putting Ed25519 on the EVM. While you can technically implement it in EVM, it's just too gas-heavy. It's best to extend the EVM itself to do more. That's the thing about having the EVM be Turing-complete, it makes people think that "it can do anything and thus abstracts over the problem thus solving it." This is technically true but not practically true -- all you are doing is punting a huge number problems/required features (like dispatch and module loading) down the road for the language to figure out. In a gas-metered context, every feature the language adds because the EVM lacks it costs gas and thus makes a number of features impossible in practice. > In fact there is already a project underway to create a verifiable programming language for the EVM. Mind linking me to it? I collect references to smart contract languages at this point and haven't heard of this one. I know the people working on the EVM + solidity formal verification project personally (well some of them at least) and it's still years away. [1]: Great technical discussion about EVM here -- https://news.ycombinator.com/item?id=14689792 https://news.ycombinator.com/item?id=14689792